6 citations · 16 across the 11 of their papers we have counts for
16 papers
Generalized Decidability via Brouwer Trees
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh +1
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable…
The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
Tom de Jong, Nicolai Kraus, Axel Ljungström
Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can…
Examples and counterexamples of injective types
Tom de Jong, Martín Hötzel Escardó
It is known that, in univalent mathematics, type universes, the type of -types in a universe, reflective subuniverses, and the underlying type of any algebra of the lifting mona…
A study of Kock's fat Delta
Tom de Jong, Nicolai Kraus, Simona Paoli +1
Motivated by the study of weak identity structures in higher category theory we explore the fat Delta category, a modification of the simplex category introduced by J. Kock and pro…
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…
Domain Theory in Constructive and Predicative Univalent Foundations
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…
Set-Theoretic and Type-Theoretic Ordinals Coincide
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary…
Sharp Elements and Apartness in Domains
Tom de Jong
Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of s…
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…
Apartness, sharp elements, and the Scott topology of domains
Tom de Jong
Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of s…
Domain Theory in Constructive and Predicative Univalent Foundations
Tom de Jong, Martín Hötzel Escardó
We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and pr…
The Sierpinski Object in the Scott Realizability Topos
Tom de Jong, Jaap van Oosten
We study the Sierpinski object in the realizability topos based on Scott's graph model of the -calculus. Our starting observation is that the object of realizers in this top…
The Scott model of PCF in univalent type theory
Tom de Jong
We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF,…