Outputs (6)

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.

The long exact sequence of homotopy n-groups (2023)
Journal Article
Buchholtz, U., & Rijke, E. (2023). The long exact sequence of homotopy n-groups. Mathematical Structures in Computer Science, 33(Special Issue 8: Homotopy Type Theory 2019), 679-687. https://doi.org/10.1017/S0960129523000038

Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence F→E→BF→E→B of pointed types and show that any fiber sequence F↪E↠BF↪E↠B of arbitrary types induces a short sequence

Fn−1 En−1 Bn−1

that is n-exact at... Read More about The long exact sequence of homotopy n-groups.

Synthetic fibered (∞,1)-category theory (2023)
Journal Article
Buchholtz, U., & Weiberger, J. (2023). Synthetic fibered (∞,1)-category theory. Higher Structures, 7(1), 74-165. https://doi.org/10.21136/HS.2023.04

We study cocartesian fibrations in the setting of the synthetic (∞,1)-category theory developed in simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.

Construction of the circle in UniMath (2021)
Journal Article
Bezem, M., Buchholtz, U., Grayson, D. R., & Shulman, M. (2021). Construction of the circle in UniMath. Journal of Pure and Applied Algebra, 225(10), Article 106687. https://doi.org/10.1016/j.jpaa.2021.106687

We show that the type TZ of Z-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-al... Read More about Construction of the circle in UniMath.