NOTE: Homotopy Type Theory
這篇是我對 HoTT(Homotopy Type Theory)目前的理解與整理,如有錯漏歡迎提出修正。
要理解就要先知道 identity 問題,即 x ≡ y
這樣的型別,在 extensional
type theory(e.g. MLTT) 裡面是唯一的,即對 P Q : x ≡ y
可以證明 P ≡ Q
UIP : (X : Set) → ∀{x x' : X} → ∀(r s : x ≡ x') → r ≡ s UIP X {x} {.x} refl refl = refl
這個性質叫做 Uniqueness of Identity Proofs,簡稱 UIP。Axiom K 跟它的關係是 K -> UIP 且 UIP -> K,因此 agda 給了一個 option 叫 without K 來取消這個 axiom。
但這樣一來我們就沒辦法表示一些 topology,比如說 circle。因為 identity 在
HoTT 裡對應的解釋是一個 path, x ≡ y
就是 x
到 y
的路徑,而
P Q : x ≡ y
自然就是 x
到 y
的兩條路徑,如果 P ≡ Q
可證明,那
P
就跟 Q
可以替換,於是你可以先變成一條線,再收縮成一個點。circle
需要的兩條路徑就沒辦法成立。有些拓墣就沒辦法表示
另一個重要的性質是 n-types
- 從 -2 的 contractible。繼續往下也是 contractible,contractible 即一個與點同倫的型別
- 到 -1 proposition
- 0 set
- 1 groupoid
- 往上可以無限加,這就是 hlevel
1. 待理解
- truncation
- univalence