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

1. 從 -2 的 contractible。繼續往下也是 contractible，contractible 即一個與點同倫的型別
2. 到 -1 proposition
3. 0 set
4. 1 groupoid
5. 往上可以無限加，這就是 hlevel