3 papers
cs.LO2026
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…
cs.LO2026
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…
cs.LO2025
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: $(\…