21 citations · 25 across the 15 of their papers we have counts for
18 papers
The -category of -categories in simplicial type theory
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about -categories. Initial work on simplicial type th…
The Yoneda embedding in simplicial type theory
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\…
Directed univalence in simplicial homotopy type theory
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applicatio…
Primitive Recursive Dependent Type Theory
Ulrik Buchholtz, Johannes Schipp von Branitz
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 -types ensures that all def…
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus +1
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form . The case of the circle has a slick answer: th…
Epimorphisms and Acyclic Types in Univalent Foundations
Ulrik Buchholtz, Tom de Jong, Egbert Rijke
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 syn…