The univalence axiom

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-15.
Last modified on 2024-02-06.

module foundation-core.univalence where
open import foundation.action-on-identifications-functions
open import foundation.fundamental-theorem-of-identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families


The univalence axiom characterizes the identity types of universes. It asserts that the map (A = B) → (A ≃ B) is an equivalence.

In this file, we define the statement of the axiom. The axiom itself is postulated in foundation.univalence as univalence.

Univalence is postulated by stating that the canonical comparison map

  equiv-eq : A = B → A ≃ B

from identifications between two types to equivalences between them is an equivalence. Although we could define equiv-eq by pattern matching, due to computational considerations, we define it as

  equiv-eq := equiv-tr (id_𝒰).

It follows from this definition that equiv-eq refl ≐ id-equiv, as expected.


Equalities induce equivalences

module _
  {l : Level}

  equiv-eq : {A B : UU l}  A  B  A  B
  equiv-eq = equiv-tr id

  map-eq : {A B : UU l}  A  B  A  B
  map-eq = map-equiv  equiv-eq

  compute-equiv-eq-refl :
    {A : UU l}  equiv-eq (refl {x = A})  id-equiv
  compute-equiv-eq-refl = refl

The statement of the univalence axiom

An instance of univalence

instance-univalence : {l : Level} (A B : UU l)  UU (lsuc l)
instance-univalence A B = is-equiv (equiv-eq {A = A} {B = B})

Based univalence

based-univalence-axiom : {l : Level} (A : UU l)  UU (lsuc l)
based-univalence-axiom {l} A = (B : UU l)  instance-univalence A B

The univalence axiom with respect to a universe level

univalence-axiom-Level : (l : Level)  UU (lsuc l)
univalence-axiom-Level l = (A B : UU l)  instance-univalence A B

The univalence axiom

univalence-axiom : UUω
univalence-axiom = {l : Level}  univalence-axiom-Level l


The univalence axiom implies that the total space of equivalences is contractible

  is-torsorial-equiv-based-univalence :
    {l : Level} (A : UU l) 
    based-univalence-axiom A  is-torsorial  (B : UU l)  A  B)
  is-torsorial-equiv-based-univalence A UA =
    fundamental-theorem-id'  B  equiv-eq) UA

Contractibility of the total space of equivalences implies univalence

  based-univalence-is-torsorial-equiv :
    {l : Level} (A : UU l) 
    is-torsorial  (B : UU l)  A  B)  based-univalence-axiom A
  based-univalence-is-torsorial-equiv A c =
    fundamental-theorem-id c  B  equiv-eq)

The underlying map of equiv-eq evaluated at ap B is the same as transport in the family B

For any type family B and identification p : x = y in the base, we have a commuting diagram

    (B x = B y) ---------> (B x ≃ B y)
         ∧                      |
  ap B p |                      | map-equiv
         |                      ∨
      (x = y) -----------> (B x → B y).
                  tr B p
module _
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} {x y : A}

  compute-equiv-eq-ap :
    (p : x  y)  equiv-eq (ap B p)  equiv-tr B p
  compute-equiv-eq-ap refl = refl

  compute-map-eq-ap :
    (p : x  y)  map-eq (ap B p)  tr B p
  compute-map-eq-ap p = ap map-equiv (compute-equiv-eq-ap p)

Recent changes