4 papers · 1 filter
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…
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…
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: $(\…
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…