The Cayley-Dickson Construction in Homotopy Type Theory. - Ulrik Buchholtz; Egbert Rijke (CoRR, 2016)

Varieties of Cubical Sets. - Ulrik Buchholtz; Edward Morehouse (RAMiCS, 2017)

Homotopy Type Theory in Lean. - Floris van Doorn; Jakob von Raumer; Ulrik Buchholtz (ITP, 2017)

The real projective spaces in homotopy type theory. - Ulrik Buchholtz; Egbert Rijke (LICS, 2017)

Higher Groups in Homotopy Type Theory. - Ulrik Buchholtz; Floris van Doorn; Egbert Rijke (LICS, 2018)

Construction of the Circle in UniMath. - Marc Bezem; Ulrik Buchholtz; Daniel R. Grayson (CoRR, 2019)

Cellular Cohomology in Homotopy Type Theory. - Ulrik Buchholtz; Kuen-Bang Hou (Favonia) (Log. Methods Comput. Sci., 2020)

Synthetic fibered (∞, 1)-category theory. - Ulrik Buchholtz; Jonathan Weinberger (CoRR, 2021)

Central H-spaces and banded types. - Ulrik Buchholtz; J. Daniel Christensen; Jarl G. Taxerås Flaten; Egbert Rijke (CoRR, 2023)

The long exact sequence of homotopy n-groups. - Ulrik Buchholtz; Egbert Rijke (Math. Struct. Comput. Sci., 2023)

Primitive Recursive Dependent Type Theory. - Ulrik Torben Buchholtz; Johannes Schipp von Branitz (LICS, 2024)

On symmetries of spheres in univalent foundations. - Pierre Cagne; Ulrik Torben Buchholtz; Nicolai Kraus; Marc Bezem (LICS, 2024)

Epimorphisms and Acyclic Types in Univalent Mathematics. - Ulrik Buchholtz; Tom de Jong; Egbert Rijke (CoRR, 2024)

Directed univalence in simplicial homotopy type theory. - Daniel Gratzer; Jonathan Weinberger; Ulrik Buchholtz (CoRR, 2024)

The Yoneda embedding in simplicial type theory. - Daniel Gratzer; Jonathan Weinberger; Ulrik Buchholtz (CoRR, 2025)