(A ≃ B) ≃ (A = B)
UNIVALENCE AXIOM
ua : ∏
(A,B : 𝒰)
(A ≃ B) → (A = B)
Γ ⊢ A : 𝒰
Γ ⊢ B : 𝒰
Γ ⊢ e : A ≃ B
(ua)
Γ ⊢ ua(e) : A = B
Γ ⊢ P : 𝒰 → 𝒰
(transport)
Γ ⊢ transport
P
(ua(e)) : P(A) → P(B)
UNIVALENCE
Unpacking...