HoTT的核心是目标相等性(identity types)，而不是路径等价性。更准确地说：

　　HoTT中：a = b 是类型，元素是证明这个相等的证据(路径)

　　它关心的是两个对象是否相等，而不是路径之间的等价

　　一旦承认时间的真实性，HoTT基于的同一性形而上学就确实面临根本挑战。

　　具体机制：

　　目标b的动态性破坏相等性

　　时间t: 有 a = b(t)

　　时间t+ε: b(t+ε) ≠ b(t)

　　但HoTT的相等性 a = b(t) 在t+ε时刻仍然"成立"吗?

　　如果成立，就错误地断言了 a = b(t+ε)

　　如果不成立，那么数学真理变成了时间相关的

　　路径证据的时效性问题

　　在时间t证明的 p : a = b(t)

　　在时间t+ε，这个证明p还有效吗?

　　如果有效，就错误地证明了 a = b(t+ε)

　　如果无效，那么数学证明有了"保质期"

　　身份类型的刚性

　　HoTT的身份类型建立在：

　　自反性：refl : a = a

　　但如果是 a(t)，那么 refl : a(t) = a(t) 只在瞬间成立

　　下一刻 a(t+ε) = a(t+ε) 但 a(t) ≠ a(t+ε)

　　形而上学基础的冲突：

　　传统数学/HoTT：假设数学对象是自我同一的(self-identical)

　　动态现实：对象在时间中持续差异化(differentiate)

　　但如果是 a(t)，那么 refl : a(t) = a(t) 只在瞬间成立，那么这个成立是一种特殊的成立。这个洞见别有用处，这里先不讨论。