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, 由Finster和Mimram提出,该理论提出了疲软的美元类的理论,其依据是,类型理论可被视为通用代数理论的表述。我们的主要贡献是正式证明,这种类型理论的模型与Maltsiniotis定义的薄弱的美元类非常吻合,其方法是将Grothendieeck提出的弱弱软的美元类的定义笼统化:这些理论被定义为适合猫类校对器的预示物,而猫类校准器是预期在美元类中的分类编码结构。这种比较是通过证明CATT理论类型理论的初始性预测来建立的,其方式可以表明某类依赖型理论的神经学理论有可能被概括化为神经论。