The univalence axiom

module foundation-core.univalence where

open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.identity-types
open import foundation-core.universe-levels

Idea

The univalence axiom characterizes the identity types of universes. It asserts that the map Id 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.

Statement

equiv-eq : {l : Level} {A : UU l} {B : UU l} → A ＝ B → A ≃ B
equiv-eq refl = id-equiv

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

Properties

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

abstract
  is-contr-total-equiv-UNIVALENCE :
    {l : Level} (A : UU l) →
    ((B : UU l) → UNIVALENCE A B) → is-contr (Σ (UU l) (λ X → A ≃ X))
  is-contr-total-equiv-UNIVALENCE A UA =
    fundamental-theorem-id' (λ B → equiv-eq) UA

Contractibility of the total space of equivalences implies univalence

abstract
  UNIVALENCE-is-contr-total-equiv :
    {l : Level} (A : UU l) →
    is-contr (Σ (UU l) (λ X → A ≃ X)) → (B : UU l) → UNIVALENCE A B
  UNIVALENCE-is-contr-total-equiv A c =
    fundamental-theorem-id c (λ B → equiv-eq)

Computing transport

compute-equiv-eq-ap :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x y : A}
  (p : x ＝ y) → map-equiv (equiv-eq (ap B p)) ＝ tr B p
compute-equiv-eq-ap refl = refl