4 papers · 1 filter
CaTT contexts are finite computads
Thibaut Benjamin, Ioannis Markakis, Chiara Sarti
Two novel descriptions of weak Ï-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are Ï-categories…
Generating Higher Identity Proofs in Homotopy Type Theory
Thibaut Benjamin
Finster and Mimram have defined a dependent type theory called CaTT, which describes the structure of omega-categories. Types in homotopy type theory with their higher identity typ…
Hom -categories of a computad are free
Thibaut Benjamin, Ioannis Markakis
We provide a new description of the hom functor on weak -categories, and we show that it admits a left adjoint that we call the suspension functor. We then show that the hom fu…
Invertible cells in -categories
Thibaut Benjamin, Ioannis Markakis
We study coinductive invertibility of cells in weak -categories. We use the inductive presentation of weak -categories via an adjunction with the category of computads, and…