3 papers
math.CT2026
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…
cs.LO2026
Delooping presented groups in homotopy type theory
Camil Champin, Samuel Mimram, Emile Oleon
Homotopy type theory is a logical setting based on Martin-Löf type theory in which geometric constructions and proofs can be carried out synthetically. Here, types can be interpre…
math.CT2026
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…