We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak $\omega$-categories, and we formalise this theory in the language of homotopy type theory. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use the formalisation that we provide to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the key aspects of the formalisation inherent to the theory CaTT, in particular that the absence of definitional equality greatly simplify the study, but also that specific side conditions are challenging to properly model. We present the formalisation in a way that not only handles the type theory CaTT but also all the related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular, monoidal weak $\omega$-categories. The article is accompanied by a development in the proof assistant Agda to actually check the formalisation that we present.
翻译:我们提出了最初由芬斯特和米姆拉姆介绍的CATT理论类型,以描述球状微弱的美元=omega$类别,我们用同质类型理论的语言将这一理论正式化。关于这种理论的大多数研究假设,它结构完善,满足了依赖型理论所共有的通常合成属性,而没有完全清楚和彻底地说明这些属性的确切性质。我们使用我们提供的正规化来列出和正式证明所有这些元属性,从而填补了基础方面的一个空白。我们讨论了CAT理论所固有的正式化的关键方面,特别是缺乏定义平等大大简化了研究,但具体的侧面条件对正确模型提出了挑战。我们介绍这种正规化的方式不仅处理CATT理论类型,而且处理所有具有相同结构的相关类型理论,而且我们特别表明,这种正规化为对MCDTT理论的研究提供了适当的基础基础,从而填补了基础方面的空白。我们讨论了CATT理论中描述的Global, 单项弱的美元=omega$- gregate-station。我们目前的正式分类中,该文章实际上由Agrudestratly 校准。