1. 传统观点：等式是布尔值

　　在经典数学或集合论中，一个等式 a = b 要么为真，要么为假。它是一个命题。

　　2. HoTT的革命：等式是空间(类型)

　　在HoTT中，a = b 本身是一个类型。这个类型的居民(terms)是 a 和 b 之间的证明或路径。

　　如果存在一条路径 p : a = b，我们就说 a 和 b 是相等的。

　　如果存在两条不同的路径 p, q : a = b，我们就说有两种不同的方式证明它们相等。

　　这直接将逻辑问题转化为了几何问题。

　　HoTT的三大支柱

　　1. 类型作为空间

　　每一个类型都可以被视作一个空间。该类型的居民是这个空间中的点。

　　例如，类型 Bool 可以看作两个离散的点(true 和 false)。

　　类型 Circle(圆)可以被定义为一个点 base 和一条从 base 到 base 的路径 loop。

　　2. 证明作为路径

　　如前所述，一个等式 a = b 的证明 p，就是连接点 a 和点 b 的一条路径。

　　3. 同伦作为路径间的变换

　　这是“同伦”一词的由来。如果 p 和 q 是两条从 a 到 b 的路径，那么一条“同伦” H : p ≡ q 就是一条连接路径 p 和路径 q 的“路径”。它可以被想象为在空间中将路径 p 连续地变形为路径 q 的过程（这里基实着一个最大的误解， p 连续地变形为路径 q 是为了解释方便的一个臆想，引用同伦的一个方便解释，事实上hott是直接判定的，没有这个连续的变形过程，这一点非常非常非常的重要）。

　　这引入了高阶结构：我们可以有路径(一等公民)、路径之间的路径(二等公民)、路径之间的路径之间的路径……这形成了一个无限丰富的层次结构，引入这个高阶结构，使得在现实使用时，更加精确，虽然还是近似的。

　　王牌：泛等公理

　　这是HoTT皇冠上的明珠，它体现了用几何直观来代替证明的等价。

　　内容：“同构的对象是不可区分的。”

　　数学表述：对于任意两个类型 A 和 B，有 (A ≃ B) ≃ (A = B)。

　　左边 (A ≃ B) 是“等价类型”的类型，即存在一个在某种意义上“完美”的映射 between A and B。

　　右边 (A = B) 是“恒等类型”，即 A 和 B 是同一个类型的证明。

　　泛等公理说，证明两个类型等价，等价于证明它们就是同一个类型。

　　哲学意义：它形式化了数学家的一个核心直觉——如果两个结构在所有的相关方面都完全一致(即同构，这个同构应该不是指形式，而是指本质意义)，那么它们就是同一个东西。例如，在范畴论中，我们常说“在唯一的同构意义下”，而泛等公理将这一思想提升为了数学的基石。

　　个人对HoTT的成就与局限的分析

　　成就：

　　联系逻辑与几何：它将逻辑证明与几何形变联系在一起，借用同伦学中的同伦连续形变来解释逻辑证明的同价性，把相等扩展到等价。

　　为数学提供了丰富的“相等”概念：等价也算相等。

　　其高阶路径的结构可能使模式更加精确。

　　推动了形式验证：基于HoTT的证明助手(如Agda, Coq的Cubical模式)非常强大，因为用等价扩展了相等。

　　局限：

　　HoTT的类型宇宙(U0, U1, U2...)虽然层次丰富，但本质上是一个预设的、永恒的、静态的柏拉图世界。所有类型和路径从一开始就已存在，必然要先预设是其不可摆脱的局限。

　　对“连续性”的先验依赖：其几何直观的核心——路径和同伦——依赖于一个经典的、连续的区间概念(如在Cubical类型论中的区间 I)。这借用同伦学中的几何的连续形变概念，来证明hott中的等价概念，这不是自身一个逻辑证明过程，而是一个定义。它用连续的背景空间来定义离散的证明对象。

　　HoTT的宣称：

　　"类型是空间，项是点，证明是路径"

　　-- 实际：

　　"类型是符号集合，项是符号，证明是符号序列"

　　-- 真相：

　　所谓的"几何直观"只是认知辅助，不是形式化的一部分

　　计算机实现中只有符号操作，没有真正的"空间"

　　HoTT的表面解释：

　　"同伦H : p ≡ q是p连续变形为q的过程"

　　-- 实际形式化：

　　"同伦只是一个类型：H : p = q，由自反性等规则构造"

　　-- 真相：

　　根本没有"连续变形"，只有离散的构造规则

　　所谓的"连续性"是解释时添加上去的

　　　HoTT的预设：

　　所有类型、所有路径"同时存在"

　　-- 实际形式化：

　　我们只能逐步构造，一项一项地构建

　　-- 真相：

　　"同时存在"是哲学预设，不是实践现实

　　在实践中，我们只与有限的部分交互

　　HoTT的实际引擎：构造规则

　　data ConstructionRule where

　　-- 1. 自反性规则(起点)

　　refl : (a : A) → (a = a)

　　-- 2. 对称性规则(逆路径)

　　sym : (p : a = b) → (b = a)

　　-- 3. 传递性规则(路径组合)

　　trans : (p : a = b) → (q : b = c) → (a = c)

　　-- 4. 函数应用规则

　　ap : (f : A → B) → (p : a = b) → (f a = f b)

　　-- 等等...

　　-- 注意：所有这些都是离散的规则应用