All Outputs (2)

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.

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory (2019)
Presentation / Conference
Pinyo, G., & Kraus, N. (2019, June). From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. Paper presented at TYPES 2019, Oslo, Norway

Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher groupoids... Read More about From Cubes to Twisted Cubes via Graph Morphisms in Type Theory.