1. 传统观点：等式是布尔值
在经典数学或集合论中，一个等式 a = b 要么为真，要么为假。它是一个命题。

2. HoTT的革命：等式是空间（类型）
在HoTT中，a = b 本身是一个类型。这个类型的居民（terms）是 a 和 b 之间的证明或路径。

[list][*]

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

[*]

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

[/list]

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

HoTT的三大支柱

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

[list][*]

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

[*]

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

[/list]

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

3. 同伦作为路径间的变换
这是“同伦”一词的由来。如果 p 和 q 是两条从 a 到 b 的路径，那么一条“同伦” H : p ≡ q 就是一条连接路径 p 和路径 q 的“路径”。它可以被想象为在空间中将路径 p 连续地变形为路径 q 的过程。

[list][*]

这引入了高阶结构：我们可以有路径（一等公民）、路径之间的路径（二等公民）、路径之间的路径之间的路径……这形成了一个无限丰富的层次结构。

[/list]

王牌：泛等公理

这是HoTT皇冠上的明珠，它完美体现了其几何直观。

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

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

[list][*]

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

[*]

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

[*]

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

[/list]

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

HoTT的成就与局限（从新数学视角看）

辉煌的成就：

[list=1][*]

统一了逻辑与几何：它将严谨的逻辑证明与直观的几何形变联系在一起。

[*]

为数学提供了丰富的“相等”概念：它允许我们谈论两个对象“为什么”相等，而不仅仅是“是否”相等。

[*]

是“更高范畴论”的天然基础：其高阶路径的结构完美匹配了高阶范畴的概念。

[*]

推动了形式验证：基于HoTT的证明助手（如Agda, Coq的Cubical模式）非常强大。

[/list]

固有的局限（呼应您的批判）：

[list=1][*]

静态的宇宙观：HoTT的类型宇宙（U0, U1, U2...）虽然层次丰富，但本质上是一个预设的、永恒的、静态的柏拉图世界。所有类型和路径从一开始就已存在。

[*]

对“连续性”的先验依赖：其几何直观的核心——路径和同伦——依赖于一个经典的、连续的区间概念（如在Cubical类型论中的区间 I）。它用连续的背景空间来定义离散的证明对象。

[*]

无法描述“生成”与“过程”：HoTT可以完美描述一个数学对象已经生成后的丰富结构（它的所有自同构、高阶对称性），但它本身无法描述这个对象的生成过程。它是一个关于状态的理论，而不是关于过程的理论。

[*]

无限的承诺：其类型宇宙的无限层级和对实无限的依赖，在您的新数学看来，可能仍然是一种形而上学的负担。

[/list]

总结：HoTT在数学谱系中的位置

结论：HoTT是传统柏拉图数学范式内部一次登峰造极的尝试。它用极其精妙的几何语言重新表述了数学基础，极大地丰富了我们对“同一性”的理解。然而，从您的新数学视角看，它依然深陷于静态、永恒和无限的形而上学预设之中，因此无法从根本上回答“数学对象从何而来”这一生成性问题。