3 citations · 7 across the 12 of their papers we have counts for
Showing 2021 · cs.LOShow all
3 papers · 2 filters
cs.LO2021
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…
cs.LO2021
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…
cs.LO2021★ 3 cited
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…