高阶归纳类型构造与消除规则：广群模型与依赖类型理论

本文主要探讨了广群模型在高阶归纳类型构造与消除规则以及依赖类型理论中的应用。首先，作者介绍了由Martin-Löf提出的通用恒等式I(A, a, A'J)，这是一种用于证明a和A'J在类型A中是等价元素的概念，其中A可以是任意类型，包括单位类型。这种无穷递归的结构在直觉类型论中可能导致类型层次的崩溃，但在内涵类型理论中，它却提供了丰富的表达能力。 在理论计算机科学的背景下，研究者们将焦点集中在更高的归纳类型上，特别是1-命中（level 1, 1-hit）和2-命中（level 2, 2-hit）类型。1-命中类型的构造仅限于点和路径，而2-命中的类型则增加了曲面构造。作者提出了一个一般图式的类型系统，不仅包含这些基本构造，还能处理更复杂的结构。 文中还阐述了从1-命中和2-命中构造函数类型中推导出的消除和相等规则，这些规则对于类型理论的正确性至关重要。通过这些规则，理论家能够有效地管理类型间的转换和等价关系，确保理论的自洽性。 进一步，文章构造了一个具有2-命中的依赖类型理论的广群模型。这种模型允许对类型之间的依赖进行细致的描述和处理。值得注意的是，通过特定的方法——截断广群模型（truncation of the groupoid model），作者揭示了如何通过这种方法得到具有1-命中的依赖类型理论的集模型。这表明在不同层次的归纳类型中，存在内在的联系和转换机制。 关键词“直觉类型论”、“单位类型”、“同伦类型论”和“高阶归纳类型”强调了论文的核心理论基础，而“setoids”和“groupoid”则指出了模型的具体实现形式。这篇论文不仅深化了我们对高阶归纳类型在广群模型中的理解，也为依赖类型理论的发展做出了贡献。读者可以通过www.sciencedirect.com或www.elsevier.com/locate/entcs获取这篇发表在《电子笔记》上的研究论文。