6 citations · 10 across the 8 of their papers we have counts for
4 papers · 1 filter
Formalizing equivalences without tears
Tom de Jong
This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique…
Domain theory in univalent foundations I: Directed complete posets and Scott's
Tom de Jong
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsk…
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…
Epimorphisms and Acyclic Types in Univalent Foundations
Ulrik Buchholtz, Tom de Jong, Egbert Rijke
We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of syn…