1 citations · 2 across the 3 of their papers we have counts for
3 papers
math.LO2018★ 1 cited
Extensional constructive real analysis via locators
Auke B. Booij
Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map f…
cs.LO2017
The HoTT reals coincide with the Euclidean reals
Auke Bart Booij
Escardó and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher inductive-induc…
cs.LO2017★ 1 cited
Parametricity, automorphisms of the universe, and excluded middle
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine +1
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assumin…