UP | HOME

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 就是 xy 的路徑,而 P Q : x ≡ y 自然就是 xy 的兩條路徑,如果 P ≡ Q 可證明,那 P 就跟 Q 可以替換,於是你可以先變成一條線,再收縮成一個點。circle 需要的兩條路徑就沒辦法成立。有些拓墣就沒辦法表示

另一個重要的性質是 n-types

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

1. 待理解

  1. truncation
  2. univalence
Date: 2022-04-02 Sat 00:00
Author: Lîm Tsú-thuàn