Extensional constructive real analysis via locators

DOI10.1017/S0960129520000171OpenAlexW3082715150MaRDI QIDQ5156769

Auke B. Booij

Publication date: 11 October 2021

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1805.06781

zbMATH Keywords

constructive mathematicshomotopy type theoryconstructive analysisdependent type theoryexact real arithmetic

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Type theory (03B38)

Uses Software

• Coq
• HoTT
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intermediate value theorem in constructive mathematics without choice
• Techniques of constructive analysis
• Constructivism in mathematics. An introduction. Volume II
• Formally Verified Approximations of Definite Integrals
• A lambda calculus for real analysis
• On the Cauchy Completeness of the Constructive Cauchy Reals
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: Extensional constructive real analysis via locators