依赖类型理论的形式化：以 CaTT 为例

我们介绍由 Finster 与 Mimram 最初引入以描述球状弱 $\omega$-范畴的类型理论 CaTT，并在同伦类型理论语言中形式化该理论。大多数关于此类型理论的研究假定其良构并满足依赖类型理论通常享有的语法性质，而未完全清晰彻底地说明这些性质究竟是什么。我们使用所提供的的形式化来列举并正式证明所有这些元性质，从而填补基础方面的空白。我们讨论 CaTT 理论固有的形式化关键方面，特别是缺乏定义性等式极大简化了研究，但特定边条件难以恰当建模。我们以不仅处理 CaTT 类型理论且处理所有共享相同结构的相关类型理论的方式呈现形式化，特别地我们表明此形式化为描述球状幺半弱 $\omega$-范畴的理论 MCaTT 的研究提供了恰当基础。本文附有在证明辅助器 Agda 中的开发以实际检验我们所呈现的形式化。