1 citations · 1 across the 4 of their papers we have counts for
4 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…
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
Daniel Gratzer, Håkon Gylterud, Anders Mörtberg +1
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types…