Univalence Axiom: (A ≃ B) ≃ (A = B)
Equivalence of types is equality of types — Voevodsky's revolutionary insight
What is ≃?
Transport
Univalence
Consequences