All Outputs (3)

Apartness, sharp elements, and the Scott topology of domains (2023)
Journal Article
de Jong, T. (2023). Apartness, sharp elements, and the Scott topology of domains. Mathematical Structures in Computer Science, 33(7), 573-604. https://doi.org/10.1017/S0960129523000282

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 sharp elements. Being apart is a positive formulation of being unequal,... Read More about Apartness, sharp elements, and the Scott topology of domains.

Set-Theoretic and Type-Theoretic Ordinals Coincide (2023)
Presentation / Conference
KRAUS, N., de Jong, T., Nordvall Forsberg, F., & Xu, C. (2023, June). Set-Theoretic and Type-Theoretic Ordinals Coincide. Paper presented at Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, USA

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 relation. We show that the two definitions are equivalent if we use (... Read More about Set-Theoretic and Type-Theoretic Ordinals Coincide.

On Small Types in Univalent Foundations (2023)
Journal Article
de Jong, T., & Escardó, M. H. (2023). On Small Types in Univalent Foundations. Logical Methods in Computer Science, 19(2), 8:1-8:33. https://doi.org/10.46298/LMCS-19%282%3A8%292023

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... Read More about On Small Types in Univalent Foundations.