9 citations · 15 across the 5 of their papers we have counts for
5 papers
Continuous and algebraic domains in univalent foundations
Tom de Jong, Martín Hötzel Escardó
We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setti…
Patch Locale of a Spectral Locale in Univalent Type Theory
Ayberk Tosun, Martín Hötzel Escardó
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…
Higher-order Games with Dependent Types
Martín Escardó, Paulo Oliva
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this wor…
Type Theory with Explicit Universe Polymorphism (revised and extended version)
Marc Bezem, Thierry Coquand, Peter Dybjer +1
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on e…
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 resi…