Showing cs.LOShow all
3 papers · 1 filter
cs.LO2024
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…
cs.LO2023★ 1 cited
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…
cs.LO2022
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…