7 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. T…
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 allow…
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…
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…
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…
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…