Homotopy Type Theory
Homotopy Type Theory
复制标题
同伦型理论
DOI：
10.1007/978-3-662-45824-2_1
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
S. Awodey
中科院分区：
文献类型：
--
作者：
S. Awodey
同伦类型理论是构造类型理论的一种新的同伦解释。它构成了最近提出的“一元数学基础”计划的基础。与计算证明助手相结合，并包括一个新的基础公理——一价公理——该程序有可能改变数学和计算机科学的理论基础，并影响科学家的实践。本次演讲将调查该领域并报告一些最新进展。
Homotopy Type Theory is a new, homotopical interpretation of constructive type theory. It forms the basis of the recently proposed Univalent Foundations of Mathematics program. Combined with a computational proof assistant, and including a new foundational axiom – the Univalence Axiom – this program has the potential to shift the theoretical foundations of mathematics and computer science, and to affect the practice of working scientists. This talk will survey the field and report on some of the recent developments.