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 for a concise description of the "walking equivalence" as a context, and of a set of maps characterising $ω$-equifibrations as substitutions. We provide an implementation of our theory, which we use to formalise basic properties of invertible cells. These properties allow us to give semantics of ICaTT in marked weak $ω$-categories, building a fibrant marked $ω$-category out of every model of ICaTT.

翻译：我们提出了依赖类型理论 CaTT 的一个保守扩展 ICaTT，用于弱 $ω$-范畴，该扩展包含一个见证单元余归纳可逆性的类型。此扩展允许将“行走等价”简洁地描述为一个上下文，并将一组刻画 $ω$-等纤维化的映射描述为代换。我们提供了该理论的实现，并利用它形式化了可逆单元的基本性质。这些性质使我们能够在标记弱 $ω$-范畴中给出 ICaTT 的语义，从每个 ICaTT 模型中构建出一个纤维性的标记 $ω$-范畴。