3 citations · 7 across the 12 of their papers we have counts for
4 papers · 1 filter
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…
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…