34 citations · 50 across the 9 of their papers we have counts for
11 papers
Compact totally separated types
Martín Hötzel Escardó
Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searc…
Internal Effectful Forcing in System T
Martin H. Escardo, Bruno da Rocha Paiva, Vincent Rahli +1
The effectful forcing technique allows one to show that the denotation of a closed System T term of type in the set-theoretical model is a continuous function $(\m…
The Patch Topology in Univalent Foundations
Igor Arrieta, Martín Hötzel Escardó, Ayberk Tosun
Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previo…
Kreisel's counter-example to full abstraction of the set-theoretical model of Goedel's system T
Martin Escardo
The set-theoretical model of Goedel's system T is not fully abstract. We also briefly discuss fully abstract models of system T.
The Cantor-Schröder-Bernstein Theorem for -groupoids
Martín Hötzel Escardó
We show that the Cantor-Schröder-Bernstein Theorem for homotopy types, or -groupoids holds in the following form: For any two types, if each one is embedded into the other,…
Intersections of compactly many open sets are open
Martín Hötzel Escardó
By definition, the intersection of finitely many open sets of any topological space is open. Nachbin observed that, more generally, the intersection of compactly many open sets is…
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…
Notions of Anonymous Existence in Martin-Löf Type Theory
Nicolai Kraus, Martín Escardó, Thierry Coquand +1
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedber…
The Herbrand Functional Interpretation of the Double Negation Shift
Martin Escardo, Paulo Oliva
This paper considers a generalisation of selection functions over an arbitrary strong monad , as functionals of type . It is assumed throughout that…
Bar Recursion and Products of Selection Functions
Martin Escardo, Paulo Oliva
We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, f…
Exhaustible sets in higher-type computation
Martin Escardo
We say that a set is exhaustible if it admits algorithmic universal quantification for continuous predicates in finite time, and searchable if there is an algorithm that, given any…