在数理逻辑与计算机科学中，同伦类型论（homotopy type theory，缩写 HoTT）是一套旨在于同伦论的大框架下构建内涵类型论语义的理论，尤指Quillen模型范畴和弱分解系统。反而言之，内涵类型论则为同伦理论提供了一套逻辑语言。类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言。^[1]

历史

1908年，恩斯特·策梅洛提出了被称作策梅洛-弗兰克尔集合论（或ZFC）的公理化集合论。该理论采用了选择公理，并作为数学的基础理论存在，因所有的数学对象均可通过集合论中的概念来解释。^[1]而英国哲学家和逻辑学家伯特兰·罗素则提出了类型论作为集合论的替代理论。^[1]

同伦理论在2002年菲尔兹奖获得者、弗拉基米尔·沃埃沃德斯基关于米尔诺猜想的工作中发挥了重要作用。 沃埃沃德斯基近年来致力于使用一价语义构造新数学基础的理论体系 UniMath，利用证明辅助工具 Coq 实现。^[1]

普林斯顿高等研究院从2012-2013年间开始致力于同伦类型论的开发，组织者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人，吸引了大量数学家和计算机科学家加入。

目前该领域亟待解决的问题包括同伦类型论的计算释义，以及开发新的、能够更好支持同伦类型论的计算机证明辅助系统。

定理证明

数学定理的证明必须遵从逻辑的原则，从公理或已证明的命题推导。而数学基础研究之终极目的是形式化一切公理，从而使所有数学定理能够精确、无二义性地推导得出。^[1]

HoTT 简化了证明助手将数学证明翻译到计算机程序语言的步骤，这为计算机检验复杂的证明提供了一条简单易行的途径。^[1]

HoTT 引入了泛等公理（univalence axiom），将同伦论与逻辑命题的等价性联系起来。该等价性同样适用于数学和计算机语言的释义，它在同伦论中能够更好地被形式化。

Homotopy Type Theory

作为该理论研究的产物，一本开放源码的书籍 Homotopy Type Theory: Univalent Foundations of Mathematics（同伦类型论：数学的泛等基础） （页面存档备份，存于互联网档案馆） 得以公开发布。作为一部纯数学作品，它非常罕见地在 GitHub 上通过社区合作的方式进行创作，并使用 Creative Commons 授权，从而允许任何人免费下载或选择购买纸质版。

参见

• 泛等基础
• 数学基础
• 同伦论
• Coq
• 弗拉基米尔·沃埃沃德斯基 – UniMath（Univalent Foundations of Mathematics） 研究项目的发起人。
• 构造演算
• 直觉类型论
• 柯里-霍华德同构

扩展阅读

• Homotopy Type Theory: Univalent Foundations of Mathematics （页面存档备份，存于互联网档案馆）. The Univalent Foundations Program. Institute for Advanced Study.
• Awodey, Steve. Type theory and homotopy. Dybjer, P.; Lindström, Sten; Palmgren, Erik; Sundholm, G. (编). Epistemology versus Ontology (PDF). Logic, Epistemology, and the Unity of Science. Springer Netherlands. 2012: 183–201 [2014-09-15]. ISBN 978-94-007-4434-9. doi:10.1007/978-94-007-4435-6_9. （原始内容存档 (PDF)于2019-07-13）. 
• Martin Hofmann and Thomas Streicher (1996), The groupoid interpretation of type theory （页面存档备份，存于互联网档案馆）, in Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, October 19–21, 1995.
• Michael A. Warren (2008), Homotopy theoretic aspects of constructive type theory （页面存档备份，存于互联网档案馆）, Ph.D. thesis, Carnegie Mellon University.
• S. Awodey and M. A. Warren (2009), Homotopy theoretic models of identity types （页面存档备份，存于互联网档案馆）, Mathematical Proceedings of the Cambridge Philosophical Society.
• Egbert Rijke (2012) Homotopy Type Theory （页面存档备份，存于互联网档案馆）, Masters Thesis, Utrecht University.

参考文献

1. ^ ^{1.0 1.1 1.2 1.3 1.4 1.5} Meyer, Florian. A new foundation for mathematics. R&D Magazine. 9/3/14 [9/6/14]. （原始内容存档于2015-09-24）.  请检查|access-date=, |date=中的日期值 (帮助)

外部链接

• Homotopy Type Theory （页面存档备份，存于互联网档案馆）
• Vladimir Voevodsky's webpage on the Univalent Foundations （页面存档备份，存于互联网档案馆）
• Homotopy Type Theory and the Univalent Foundations of Mathematics （页面存档备份，存于互联网档案馆） by Steve Awodey
• "Constructive Type Theory and Homotopy" （页面存档备份，存于互联网档案馆） – Video lecture by Steve Awodey at the Institute for Advanced Study
• Homotopy Type Theory Google GroupPortuguese Web Archive的存档，存档日期2011-01-22
• Homotopy Type Theory IRC channel