2013 同倫型別論迷案：Voevodsky 的 Univalence 改寫相等#

報案人：數學基礎。案情：什麼叫「相等」？集合論的答案不夠用了。 偵探：Vladimir Voevodsky。兇器：Univalence 公理與《HoTT Book》。

案發現場#

2013 年之前，數學界表面平靜，實則暗潮洶湧。集合論的 ZFC 基礎雖然強大，卻有兩個懸案始終未破：

• 計算機無法理解集合論。ZFC 的語言是非構造性的，證明存在卻給不出算法，證明助理難以直接採用。
• 同倫論學家每天都在做「同倫等價即相等」的事，卻在基礎層面被視為非法。用拓樸學家的話說，咖啡杯和甜甜圈「一樣」，但集合論卻說它們「不一樣」。

2006 年，菲爾茲獎得主 Voevodsky 在研究動機上同調時遭遇了一場個人危機：他發現自己早年的一篇論文證明有誤，而錯誤竟多年無人察覺。他開始追問：如果連頂尖數學家的證明都不可靠，數學的根基該放在哪裡？

他的回答出人意料：把型別看成空間，把相等看成路徑。這就是同倫型別論（Homotopy Type Theory，簡稱 HoTT）的起點。

2012 至 2013 年，普林斯頓高等研究院聚集了一批邏輯學家、拓樸學家與計算機科學家，集體撰寫了《Homotopy Type Theory: Univalent Foundations of Mathematics》，即著名的 HoTT Book，並於 2013 年公開。這本書既是教科書，也是一份「新基礎宣言」。

偵查過程#

線索一：型別即空間，相等即路徑#

在 Martin-Löf 型別論中，每個型別 \(A\) 都配有一個相等型別 \(Id_{A}(x, y)\) ，通常記為 \(x =_{A} y\) 。傳統上大家把它當成「命題」：要麼成立，要麼不成立。

HoTT 的關鍵翻轉是：把 \(x =_{A} y\) 看成「從 \(x\) 到 \(y\) 的路徑空間」。於是：

• 元素 \(p : x =_{A} y\) 是一條路徑。
• 兩個路徑 \(p, q\) 之間還可以有高維路徑 \(r : p = q\) ，如同路徑之間的同倫。
• 型別 \(A\) 因此具有無窮維的群胚結構，即所謂的無窮群胚。

路徑歸納（path induction）是整個理論的偵查手冊。它斷言：要證明關於任意路徑 \(p : x =_{A} y\) 的性質 \(P\) ，只需處理自反路徑 \(refl_{x} : x =_{A} x\) 的情形。其規則可寫為：

這就像偵探說：只要搞清楚「留在原地」的案子，所有「從甲地到乙地」的案子都自動破解。

線索二：Univalence 公理——本案的核心兇器#

Voevodsky 提出的單值性（univalence）公理斷言：型別之間的相等，等價於型別之間的等價。形式化地說，對任意型別 \(A\) 與 \(B\) ，存在典範映射 \(idtoeqv\) ，且它是等價：

其中左邊的 \(A = B\) 是宇宙 \(U\) 中的路徑型別，右邊的 \(A \simeq B\) 是同倫等價型別。更直白地說，同構的結構在此基礎中就是相等的。

這條公理在 ZFC 中是不可想像的：兩個同構的集合在 ZFC 裡通常並不相等。但在數學實踐中，數學家本來就把同構的對象視為同一。Univalence 只是把「潛規則」扶正為「明法條」。

它的威力可以列表如下：

舉例來說，若 \(e : A \simeq B\) 是一個等價，則由 \(ua\) 得到路徑 \(ua(e) : A = B\) ，於是對任意型別族 \(P\) ，都有傳輸函數 \(transport^{P}(ua(e)) : P(A) \to P(B)\) 。數學結構沿等價的搬運從此天經地義。

線索三：高維相等與截斷階層#

一旦接受路徑可以有多層，型別就有了「同倫層次」（h-level）：

• 契約型別（contractible）：只有一個點，如單點空間。
• 命題（proposition）：任意兩點間至多一條路徑，對應傳統邏輯命題。
• 集合（set）：相等型別都是命題，對應傳統集合。
• 群胚（groupoid）：相等型別是集合，容許非平凡對稱。
• 更高層次以此類推，直至無窮。

傳統數學只住在第 2 層，而 HoTT 打開了整棟大樓。命題截斷 \(||A||\) 、集合截斷 \(||A||_{0}\) 等構造，讓偵探可以自由選擇「要看到多精細的證據」。

HoTT Book 用這種語言重建了同倫論的基本定理，包括基本群的計算、Freudenthal 懸垂定理，甚至給出了 \(\pi_{n}(S^{n})\) 的構造性證明。

結案報告#

2013 年的 HoTT Book 並沒有「終結」數學基礎之爭，但它成功立案了一個全新的平行調查方向：

• 新基礎候選：單值基礎（Univalent Foundations）成為 ZFC 之外最有系統的新基礎計畫，直接催生了 Voevodsky 的後續研究。
• 證明助理的革新：傳統的 Coq 與 Agda 無法原生計算 univalence，於是催生了 Cubical Type Theory 與 Cubical Agda，讓 \(ua\) 從公理變成可計算的定理。
• 數學與程式的和解：同一個語言既能講同倫論，又能被機器執行，Curry-Howard 對應被推向高維。
• 未解的尾巴：Univalence 與構造性的相容問題、語意模型問題，留給了 2015 年後的立方（cubical）偵探們繼續追查，也為本書後續的 Lean 與 AI 證明埋下伏筆。

用探案術語說：Voevodsky 沒有抓到舊兇手，而是證明了應該換一間警局辦案。

證據與工具#

證據一：Univalence 的 Agda 風格表述

postulate ua : {A B : Type} → (A ≃ B) → (A ≡ B)

其中 \(A ≃ B\) 表示同倫等價， \(A ≡ B\) 表示相等型別。完整的公理還要求 \(ua\) 本身是等價，即 \(idtoeqv\) 與 \(ua\) 互逆。

證據二：路徑歸納的推理規則表

證據三：偵探工具箱

延伸閱讀：《Homotopy Type Theory: Univalent Foundations of Mathematics》（Institute for Advanced Study，2013）；Voevodsky "An Experimental Library of Formalized Mathematics"（2010）。