作为某类型论模型的球状弱ω-范畴
Globular weak $ω$-categories as models of a type theory
AI总结：
本研究针对表述弱ω-范畴理论的依赖类型论CaTT，通过证明其初始性猜想，形式化验证了该类型论的模型与Maltsiniotis定义的球状弱ω-范畴精确对应，为相关类型论的神经定理推广提供了可能。
摘要：
我们遵循“类型论可被视为广义代数理论的表示”这一思路，研究由Finster和Mimram提出的、表述弱ω-范畴理论的依赖类型论CaTT。我们的核心贡献是一项形式化证明：该类型论的模型恰好对应Maltsiniotis定义的弱ω-范畴——后者是对Grothendieck提出的弱ω-广群定义的推广，被定义为cat-coherator（范畴-共合子，一种编码了ω-范畴中预期存在的结构的范畴）上的合适预层。这一对应关系是通过证明CaTT类型论的初始性猜想建立的，该证明方式表明相关结论或可推广为某一类依赖类型论的神经定理。
英文摘要：
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 as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $ω$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $ω$-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
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
