2 citations · 4 across the 9 of their papers we have counts for
9 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…
Internal sums for synthetic fibered -categories
Jonathan Weinberger
We give structural results about bifibrations of (internal) -categories with internal sums. This includes a higher version of Moens' Theorem, characterizing cartesian b…
Two-sided cartesian fibrations of synthetic -categories
Jonathan Weinberger
Within the framework of Riehl-Shulman's synthetic -category theory, we present a theory of two-sided cartesian fibrations. Central results are several characterizations…
Strict stability of extension types
Jonathan Weinberger
The theory of -categories can be developed synthetically in an augmentation of homotopy type theory introduced by Riehl--Shulman. Central to their development is an add…
A Synthetic Perspective on -Category Theory: Fibrational and Semantic Aspects
Jonathan Weinberger
Reasoning about weak higher categorical structures constitutes a challenging task, even to the experts. One principal reason is that the language of set theory is not invariant und…
Synthetic fibered -category theory
Ulrik Buchholtz, Jonathan Weinberger
We study cocartesian fibrations in the setting of the synthetic -category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our developmen…
Simplicial sets inside cubical sets
Thomas Streicher, Jonathan Weinberger
As observed recently by various people the topos of simplicial sets appears as essential subtopos of a topos of cubical sets, namely presheaves over…