两层类型论与应用
摘要：我们定义和发展了两级类型理论（2LTT），这是Martin-L"of类型理论的一个版本，结合了两种不同的类型理论。我们将其称为内部和外部类型理论。在我们感兴趣的情况下，内部理论是同伦类型理论（HoTT），可以包括等价宇宙和高阶归纳类型。外部理论是传统类型理论的形式，验证了恒等证明的唯一性（UIP）。其中一种观点是将其视为内部类型理论的内在化元理论。 2LTT有两个动机。首先，关于HoTT的某些结果是元理论性质的，例如在外部固定自然数n的情况下，可以构造出HoTT中的n级半加性类型。这样的结果无法在HoTT本身中表达，但它们可以在2LTT中进行形式化和证明，其中n将是外部理论中的一个变量。这种观点受到预层模型保守性的观察的启发。 其次，2LTT是一个适合于形式化想要添加到HoTT的附加公理的框架。这个思想在很大程度上受到Voevodsky的同伦类型系统（HTS）的启发，它构成了2LTT的一个具体实例。HTS具有一个保证自然数类型的公理，使其行为类似于外部自然数，从而允许构造半加性类型的宇宙。在2LTT中，这个公理可以简单地要求内部和外部自然数是同构的。 在定义了2LTT之后，我们建立了一系列工具，目标是使2LTT成为未来发展的一个便利语言。作为第一个应用，我们以Shulman的风格开发了Reedy纤维图的理论。在继续思考这一思路的同时，我们提出了（无穷，1）-范畴的定义并给出了一些例子。
作者：Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler
论文ID：1705.03307
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-13