3 citations · 7 across the 12 of their papers we have counts for
12 papers
Computads with invertible generators for weak ω-categories
Thibaut Benjamin, Camil Champin, Ioannis Markakis
We extend the notion of computads for weak \(ω\)-categories to allow marking certain generators as invertible, and describe inductively the free \(ω\)-categories they generate. Thi…
A type theory for invertibility in weak -categories
Thibaut Benjamin, Camil Champin, Ioannis Markakis
We present a conservative extension ICaTT of the dependent type theory CaTT for weak -categories with a type witnessing coinductive invertibility of cells. This extension allows…
AdapTT: Functoriality for Dependent Type Casts
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin +1
The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradua…
Beyond Eckmann-Hilton: Commutativity in Higher Categories
Thibaut Benjamin, Ioannis Markakis, Wilfred Offord +2
We show that in a weak globular -category, all composition operations are equivalent and commutative for cells with sufficiently degenerate boundary, which can be considered a h…
Naturality for higher-dimensional path types
Thibaut Benjamin, Ioannis Markakis, Wilfred Offord +2
We define a naturality construction for the operations of weak omega-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a…
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…
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 s…
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.…
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 fun…
Formalization of dependent type theory: The example of CaTT
Thibaut Benjamin
We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak -categories, and we formalise this theory in the language of homotopy type…
Monoidal weak omega-categories as models of a type theory
Thibaut Benjamin
Weak -categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored, based on different shapes given…
Globular weak -categories as models of a type theory
Thibaut Benjamin, Eric Finster, Samuel Mimram
We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak -categories, following the idea that type theories can be considered…