Search

• < Previous
• 1
• Next >

---

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 continuous predicate, either selects an element for which the predicate holds or else tells there is no example. The&nbsp;[&hellip;]

---

Notions of Anonymous Existence in Martin-L\"of Type Theory

Nicolai Kraus ; Martín Escardó ; Thierry Coquand ; Thorsten Altenkirch.

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these&nbsp;[&hellip;]

---

On Small Types in Univalent Foundations

Tom de Jong ; Martín Hötzel Escardó.

We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot&nbsp;[&hellip;]

---