Definition·独立条目
同伦类型论的类型—空间对应
The Types-as-Spaces Correspondence
同伦类型论仍在发展中，具体的形式系统（如立方类型论）与本条目描述的可能存在差异； 本条目只覆盖基本的类型—空间对应与单价公理。
01
严格数学表述
Statement
在马丁–洛夫类型论的同伦解释下：
- 类型 解释为空间（同伦类型）；
- 项 解释为该空间的点；
- 等词类型 解释为从 到 的道路空间；
- 等词的证明 解释为一条道路； 解释为同伦。
类型等价（存在双向映射且两复合同伦于恒等）对应同伦等价。 单价公理断言等价与相等本身等价：
02
成立条件与适用对象
Conditions & Scope
成立条件
在马丁–洛夫类型论（MLTT）的框架内
单价公理是额外公理，不是 MLTT 的定理
适用对象
类型论同伦类型
03
定义解释
Explanation
这一对应不是把类型「看成」集合，而是把类型「看成」空间： 等词类型具有道路空间的结构，因此相等本身可以携带高阶信息（两条相等之间的相等、等等）。 单价公理把「同构的对象可以互相替换」这一数学实践变成可形式化的原则。
042 个
前置概念
Prerequisites
061 条
参考来源
References
- [1]The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.专著 · Ch. 2 (同伦与等价)https://homotopytypetheory.org/book/已审核