同伦类型论

在数理逻辑和计算机科学中，同伦类型理论 (HoTT /hɒt/) 是指直觉类型理论的各种发展路线，基于将类型解释为（抽象）同伦理论直觉适用的对象。

除其他工作外，这包括为此类类型理论构建同伦模型和更高分类模型； 使用类型论作为抽象同伦论和更高范畴论的逻辑（或内部语言）； 在类型论基础上发展数学（包括以前存在的数学和同伦类型使之成为可能的新数学）； 以及计算机证明助手中每一个的形式化。

被称为同伦类型理论的工作与单价基础项目之间存在很大的重叠。 尽管两者都没有被精确描述，并且这些术语有时可以互换使用，但用法的选择有时也对应于观点和重点的差异。 因此，本文可能无法平等地代表该领域所有研究人员的观点。 当一个领域处于快速变化中时，这种可变性是不可避免的。

有一段时间，内涵类型理论中的类型及其身份类型可以被视为类群的想法是数学民间传说。 它在 1998 年 Martin Hofmann 和 Thomas Streicher 的论文中首次在语义上进行了精确描述，该论文名为类型理论的群群解释，在该论文中，他们表明内涵类型理论在群群类别中有一个模型。 这是类型论的xxx个真正的同伦模型，尽管只是一维的（集合范畴中的传统模型是同伦 0 维的）。

他们的论文还预示了同伦类型理论后来的几个发展。 例如，他们注意到类群模型满足一个他们称为宇宙外延性的规则，这正是 Vladimir Voevodsky 十年后提出的对单价公理 1 类型的限制。 （然而，1-类型的公理显然更容易表述，因为不需要一致的等价概念。）他们还将具有同构的类别定义为相等，并推测在使用高维类群的模型中，对于此类类别，一 本来等价就是平等； 这后来被 Benedikt Ahrens、Krzysztof Kapulkin 和 Michael Shulman 证明了。

内涵类型理论的xxx个高维模型是由 Steve Awodey 和他的学生 Michael Warren 在 2005 年使用 Quillen 模型类别构建的。 这些结果首次在 FMCS 2006 会议上公开展示，沃伦在会上发表了题为“内涵类型理论的同伦模型”的演讲，该演讲也作为他的论文说明书（出席论文委员会的有 Awodey、Nicola Gambino 和 Alex Simpson）。 摘要包含在 Warren 的论文招股说明书摘要中。

随后在 2006 年乌普萨拉大学举办的关于身份类型的研讨会上，有两次关于内涵类型理论和分解系统之间关系的演讲：一场由 Richard Garner 主持，类型理论的分解系统，另一场由 Michael Warren 主持，模型类别和内涵认同类型 . Steve Awodey 在高维类别的类型理论和 Thomas Streicher，身份类型与弱 omega-groupoids：一些想法，一些问题的会谈中讨论了相关的想法。 在同一次会议上，Benno van den Berg 发表了题为 Types as weak omega-categories 的演讲，他在演讲中概述了后来成为与 Richard Garner 联合论文主题的想法。

高维模型的所有早期构造都必须处理依赖类型理论模型的典型连贯性问题，并且开发了各种解决方案。 其中一个由 Voevodsky 在 2009 年给出，另一个由 van den Berg 和 Garner 在 2010 年给出。 Lumsdaine 和 Warren 最终在 2014 年给出了基于 Voevodsky 构造的通用解决方案。

在 2007 年的 PSSL86 上，Awodey 发表了题为“同伦类模型”的演讲（这是该术语的首次公开使用，由 Awodey 创造）。 Awodey 和 Warren 在论文 Homotopy theoretic theoretic models of identity types 中总结了他们的结果，该论文于 2007 年发布在 ArXiv 预印本服务器上，并于 2009 年出版； 更详细的版本出现在 Warren 2008 年的论文 Homotopy theoretic aspects of constructive type theory 中。

大约在同一时间，Vladimir Voevodsky 在寻找一种实用的数学形式化语言的背景下独立研究类型论。 2006 年 9 月，他在 Types 邮件列表上发布了关于同伦 lambda 演算的非常简短的说明，其中概述了具有相关产品、总和和全域的类型理论以及这种类型的模型 。