The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation

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

zbMATH Keywords

constructive mathematicstopos theoryhomotopy type theorydependent typefunction extensionalityanonymous existenceintensional Martin-Löf type theoryCurry-Howard interpretationBrouwerian continuity axiomspropositional truncation

Mathematics Subject Classification ID

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