The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
From MaRDI portal
Publication:5277837
DOI10.4230/LIPIcs.TLCA.2015.153zbMath1433.03030OpenAlexW2189582351MaRDI QIDQ5277837
Chuangjie Xu, Martín Hötzel Escardó
Publication date: 12 July 2017
Full work available at URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.153
constructive mathematicstopos theoryhomotopy type theorydependent typefunction extensionalityanonymous existenceintensional Martin-Löf type theoryCurry-Howard interpretationBrouwerian continuity axiomspropositional truncation
Constructive and recursive analysis (03F60) Topoi (18B25) Combinatory logic and lambda calculus (03B40) Type theory (03B38)
Related Items
AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Connectedness of the continuum in intuitionistic mathematics ⋮ On Small Types in Univalent Foundations ⋮ Unnamed Item ⋮ Type-theoretic approaches to ordinals ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Univalent polymorphism ⋮ Extensional constructive real analysis via locators ⋮ COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS ⋮ Unnamed Item ⋮ A Coalgebraic View of Bar Recursion and Bar Induction ⋮ Exercising Nuprl’s Open-Endedness ⋮ Continuous and monotone machines ⋮ Nets and reverse mathematics ⋮ Formally computing with the non-computable
This page was built for publication: The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
