We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $\omega$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $\omega$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $\omega$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $\omega$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories

翻译：摘要：本文研究由Finster和Mimram提出的依赖类型理论CaTT，该理论基于类型理论可被视为广义代数理论表示的观点，描述了弱 $ω$-范畴理论。我们的主要贡献是形式化证明：该类型理论的模型恰好对应于Maltsiniotis定义的弱 $ω$-范畴，这是通过推广Grothendieck为弱 $ω$-群胚提出的定义实现的——这些弱 $ω$-范畴被定义为某个cat-余协调器（一种编码 $ω$-范畴中预期结构的范畴）上的适当预层。这一比较通过证明类型理论CaTT的初始性猜想得以建立，其证明方式暗示了可推广至某类依赖类型理论的神经定理。