同构类型理论

在数理逻辑和计算机科学中，同构类型理论（HoTT/hɒt/）是指直观类型理论的各种发展路线，其基础是将类型解释为（抽象的）同构理论的直觉所适用的对象。这包括为这种类型理论构建同构和高分类模型；将类型理论作为抽象同构理论和高分类理论的逻辑（或内部语言）；在类型理论的基础上发展数学（包括以前存在的数学和同构类型使之成为可能的新数学）；以及在计算机证明助手中对上述每一项进行形式化。被称为同构类型理论的工作与单价基础项目之间存在着很大的重叠。虽然两者都没有精确的划分，而且这些术语有时可以互换使用，但用法的选择有时也与观点和重点的不同相对应。因此，本文可能并不完全代表这些领域所有研究者的观点。当一个领域处于快速变化之中时，这种差异性是不可避免的。

前史：群组模型曾几何时，广义类型理论中的类型及其身份类型可以被视为群组的想法是数学界的民间传说。1998年，MartinHofmann和ThomasStreicher发表了一篇名为《类型理论的类群解释》的论文，首次在语义上明确了这一观点，他们在论文中表明，广义类型理论在类群中有一个模型。这是类型理论的xxx个真正的同构模型，尽管只是一维的（集合类别中的传统模型是同构的0维）。他们的论文也预示了后来同构类型理论的若干发展。例如，他们指出类群模型满足一个他们称之为宇宙扩展性的规则，这不是别的，而是弗拉基米尔-沃耶沃茨基十年后提出的对1-类型的限制。(然而，1-类型的公理在表述上明显更简单，因为不需要一个连贯的等价概念）。他们还将同构的范畴定义为平等，并猜想在一个使用高维群的模型中，对于这样的范畴，人们会有平等性；这后来被BenediktAhrens,KrzysztofKapulkin和MichaelShulman证明。早期历史：模型类别和高分组2005年，SteveAwodey和他的学生MichaelWarren用Quillen模型类别构建了扩展类型理论的xxx个高维模型。

所有早期的高维模型的构造都必须处理依附类型理论模型的典型的一致性问题，并且开发了各种解决方案。大约在同一时间，VladimirVoevodsky在寻找数学实用形式化语言的背景下独立研究类型理论。2006年9月，他在Types邮件列表中发表了一篇关于同构λ微积分的简短说明，其中勾勒出一个具有依存积、和与宇宙的类型理论的轮廓，以及这个类型理论的一个模型.