空间 的同伦类型是 在同伦等价下的等价类。两个空间具有相同的同伦类型当且仅当它们同伦等价； 同伦不变量只依赖同伦类型，而不依赖空间的具体点集结构。
同一概念可以拥有多条定义：它们可能刻画同一对象的不同侧面（例如标准定义与范畴论刻画）。 每条定义都有独立页面与来源。
称拓扑空间 与 具有相同的同伦类型，若 （同伦等价）。 同伦类型是空间在同伦等价关系下的等价类。 一个构造 称为同伦不变量，若 蕴含 。
成立条件
同伦等价关系由同伦逆的存在性定义
「」中的同构类型依赖 的取值范畴（群、环、集合等）
适用对象
定义解释
同伦类型不是某个具体空间，而是空间在等价关系下的类。 说「 与 有相同的同伦类型」等价于「不存在任何同伦不变量能区分它们」—— 但这后一说法需要 Whitehead 定理（在 CW 复形上）才能变成可计算的条件。
参考来源：2 条（见定义页）
严格数学前置指「定义中直接使用了对方」；学习前置是教学顺序建议，二者可能不同。 所有前置概念都可以点击跳转，并可逐层递归展开。
暂无额外学习前置；上列的数学前置同时也是学习起点。
多层前置（最多展开三层，点击三角展开）
拓扑空间的数量不可穷尽，逐个分类没有希望。同伦论需要先决定「什么样的差异可以忽略」， 否则连问题的提法都不清楚。
同胚分类仍然过细： 与单点不同胚，挖去一点的平面与圆周不同胚， 但在同伦论中它们携带完全相同的信息。若不做商，同伦不变量就会被大量「无关差异」淹没。
以同伦等价为等价关系，把空间划分成同伦类型；把研究对象从「空间」替换为「型」。
同伦论的研究对象成为同伦类型：不变量是型的函数，映射的同伦类给出型之间的态射。 Whitehead 定理进一步说明，对 CW 复形，型可以由各阶同伦群完全决定。
关系按类型分开记录：逻辑依赖、学习顺序、推广与特例、应用、思想联系、历史影响。 下图以本概念为中心，点击节点可展开邻居，双击节点打开对应概念页。
由数学定义本身决定的关系：谁依赖谁、谁推广谁、谁与谁等价。这类关系与学习者无关。
requires同伦类型论把每个类型解释为同伦类型；没有同伦类型的概念，就没有类型—空间对应。
不构成严格逻辑依赖，但在思想史或方法论上互相照亮的关系。
conceptual_connection时间线中的每个事件都关联文献来源；标注「待审核」表示书目信息尚未完全核对。
Kan 引入满足「角填充条件」的单纯集（后称 Kan 复形），使得同伦群可以在纯组合的 层面定义，而不必依赖拓扑空间。这开启了抽象同伦论：同伦结构可以被编码在组合数据中， 为后来的单纯集模型与模型范畴理论铺路。
Grothendieck 在未正式出版的手稿《Pursuing Stacks》中提出以 -群胚刻画同伦型的纲领 （即「同伦假设」），并倡议发展高阶范畴与同伦代数。这条线索后来与同伦类型论的高阶结构观汇合。
《Homotopy Type Theory: Univalent Foundations of Mathematics》出版， 系统阐述类型—空间对应、等词类型作为道路空间、以及单价公理。 这使「同伦等价」从拓扑学的概念变成可以直接在证明助手中形式化的基础原则。
从这里出发可以继续探索的方向，按「直接推广 / 理论应用 / 思想联系 / 现代发展」区分。
Whitehead 定理说明：连通 CW 复形之间的同伦类型由各阶同伦群决定（在映射层面）。
Hatcher 2002
同伦类型论把「同伦类型」变成类型论的基本对象：类型被解释为空间，等价被解释为同伦等价。
Univalent Foundations Program 2013
同伦类型是「只保留同伦信息」的空间概念。它把拓扑学从研究具体点集，变成研究形变下不变的结构。 同伦类型论后来把这个想法推到逻辑层面：类型本身就是空间，而相等就是道路。
这些例子说明：同伦类型比同胚类型粗，而粗得恰好足以让代数不变量变得可计算。