All Outputs (3)

Epimorphisms and acyclic types in univalent foundations (2024)
Journal Article
Buchholtz, U., De Jong, T., & Rijke, E. (in press). Epimorphisms and acyclic types in univalent foundations. Journal of Symbolic Logic,

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 synthetic homotopy theory as developed in univalent foundations. We prese... Read More about Epimorphisms and acyclic types in univalent foundations.

On symmetries of spheres in univalent foundations (2024)
Presentation / Conference Contribution
Cagne, P., Buchholtz, U. T., Kraus, N., & Bezem, M. (2024, July). On symmetries of spheres in univalent foundations. Presented at LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Tallinn

Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form Sn = Sn. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, th... Read More about On symmetries of spheres in univalent foundations.

Primitive Recursive Dependent Type Theory (2024)
Presentation / Conference Contribution
Buchholtz, U. T., & Schipp von Branitz, J. (2024, July). Primitive Recursive Dependent Type Theory. Presented at LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Tallinn, Estonia

We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing ####II-types ensures that all definable functions are primitive recursive. This extends the concept... Read More about Primitive Recursive Dependent Type Theory.