同伦类型论把类型解释为空间、项解释为点、等词类型 解释为道路空间； 在此解释下同伦等价对应类型等价，Voevodsky 的单价公理使「等价即相等」成为可形式化的原则。
同一概念可以拥有多条定义：它们可能刻画同一对象的不同侧面（例如标准定义与范畴论刻画）。 每条定义都有独立页面与来源。
在马丁–洛夫类型论的同伦解释下：
类型等价（存在双向映射且两复合同伦于恒等）对应同伦等价。 单价公理断言等价与相等本身等价：
成立条件
在马丁–洛夫类型论（MLTT）的框架内
单价公理是额外公理，不是 MLTT 的定理
适用对象
定义解释
这一对应不是把类型「看成」集合，而是把类型「看成」空间： 等词类型具有道路空间的结构，因此相等本身可以携带高阶信息（两条相等之间的相等、等等）。 单价公理把「同构的对象可以互相替换」这一数学实践变成可形式化的原则。
参考来源：1 条（见定义页）
严格数学前置指「定义中直接使用了对方」；学习前置是教学顺序建议，二者可能不同。 所有前置概念都可以点击跳转，并可逐层递归展开。
暂无额外学习前置；上列的数学前置同时也是学习起点。
多层前置（最多展开三层，点击三角展开）
类型论中的相等是语法性的（definitional / propositional equality）， 而数学实践大量使用「在等价意义下相同」：同构的群、同伦等价的空间应当可以互相替换。
把类型读成集合时，等词类型只是相等关系，同构的对象并不相等， 因此需要大量「transport」式的手工搬运，且这些搬运本身没有原则性的地位。
用同伦论解释类型论：类型是空间，等词类型是道路空间，类型的等价（等价于同伦等价） 由单价公理提升为相等。
得到一套「同伦不变」的数学基础：等价的对象可以相互替换，且这一原则可以被证明助手检查。 同伦类型论同时成为 -范畴与高阶结构的内部语言。
关系按类型分开记录：逻辑依赖、学习顺序、推广与特例、应用、思想联系、历史影响。 下图以本概念为中心，点击节点可展开邻居，双击节点打开对应概念页。
由数学定义本身决定的关系：谁依赖谁、谁推广谁、谁与谁等价。这类关系与学习者无关。
requires同伦类型论把每个类型解释为同伦类型；没有同伦类型的概念，就没有类型—空间对应。
类型等价被定义为存在双向映射且两复合同伦于恒等，这逐字对应同伦等价。
不构成严格逻辑依赖，但在思想史或方法论上互相照亮的关系。
conceptual_connection两者都试图为「同伦结构」提供基础语言：模型范畴是外部的范畴论框架，同伦类型论是内部的类型论语言。
inspired_by把类型读成群胚（从而读成空间）的模型来自同伦论中的群胚思想；这条线索使「类型即空间」成为可验证的数学陈述，而不只是比喻。
时间线中的每个事件都关联文献来源；标注「待审核」表示书目信息尚未完全核对。
Grothendieck 在未正式出版的手稿《Pursuing Stacks》中提出以 -群胚刻画同伦型的纲领 （即「同伦假设」），并倡议发展高阶范畴与同伦代数。这条线索后来与同伦类型论的高阶结构观汇合。
《Homotopy Type Theory: Univalent Foundations of Mathematics》出版， 系统阐述类型—空间对应、等词类型作为道路空间、以及单价公理。 这使「同伦等价」从拓扑学的概念变成可以直接在证明助手中形式化的基础原则。
从这里出发可以继续探索的方向，按「直接推广 / 理论应用 / 思想联系 / 现代发展」区分。
同伦类型论把「同伦类型」提升为类型论的基本对象：每个类型都自动带有同伦结构。
Univalent Foundations Program 2013
类型等价被定义为「有同伦逆的映射」，与拓扑中的同伦等价逐字对应。
Univalent Foundations Program 2013
模型范畴与同伦类型论是处理同伦结构的两种互补语言：外部范畴论 vs 内部类型论。
Univalent Foundations Program 2013
同伦类型论把「空间」与「命题」放在同一层：类型既是集合也是空间，等词既是相等也是道路。 它让同伦论的思想进入逻辑基础，也让「等价即相等」从一条哲学原则变成可计算的公理。
| 类型论 | 同伦论 |
|---|---|
| 类型 | 空间 |
| 项 | 点 |
| 等词类型 | 从 到 的道路空间 |
| 等词的证明 | 道路 |
| 等词的等词 | 同伦 |
| 类型等价 | 同伦等价 |
| 单价公理 | 等价蕴含相等 |
它断言「等价」与「相等」本身是同伦等价的类型。这条公理不是定理，而是额外的公理， 它使同构的对象在类型论内部真正可以互相替换。
同伦类型论是活跃的研究领域；本条目只描述其基本对应与动机，不涉及具体的技术细节 （如高阶归纳类型、立方类型论等）。