# The univalence axiom

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Eléonore Mangel, Elisabeth Stenholm, Raymond Baker and Vojtěch Štěpančík.

Created on 2022-02-15.

module foundation.univalence where

open import foundation-core.univalence public

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.universe-levels

open import foundation-core.coherently-invertible-maps
open import foundation-core.contractible-types
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.torsorial-type-families


## Idea

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 postulate the univalence axiom. Its statement is defined in foundation-core.univalence.

## Postulates

Rather than postulating a witness of univalence-axiom directly, we postulate the constituents of a coherent two-sided inverse to equiv-eq. The benefits are that we end up with a single converse map to equiv-eq, rather than a separate section and retraction, although they would be homotopic regardless. In addition, this formulation helps Agda display goals involving the univalence axiom in a more readable way.

module _
{l : Level} {A B : UU l}
where

postulate
eq-equiv : A ≃ B → A ＝ B

is-section-eq-equiv : is-section equiv-eq eq-equiv

is-retraction-eq-equiv' : is-retraction equiv-eq eq-equiv

coh-eq-equiv' :
coherence-is-coherently-invertible
( equiv-eq)
( eq-equiv)
( is-section-eq-equiv)
( is-retraction-eq-equiv')

univalence : univalence-axiom
univalence A B =
is-equiv-is-invertible eq-equiv is-section-eq-equiv is-retraction-eq-equiv'


## Properties

module _
{l : Level} {A B : UU l}
where

equiv-univalence : (A ＝ B) ≃ (A ≃ B)
pr1 equiv-univalence = equiv-eq
pr2 equiv-univalence = univalence A B

abstract
is-retraction-eq-equiv : is-retraction (equiv-eq {A = A} {B}) eq-equiv
is-retraction-eq-equiv =
is-retraction-map-inv-is-equiv (univalence A B)

module _
{l : Level}
where

is-equiv-eq-equiv : (A B : UU l) → is-equiv (eq-equiv {A = A} {B})
is-equiv-eq-equiv A B =
is-equiv-is-invertible equiv-eq is-retraction-eq-equiv' is-section-eq-equiv

compute-eq-equiv-id-equiv : (A : UU l) → eq-equiv {A = A} id-equiv ＝ refl
compute-eq-equiv-id-equiv A = is-retraction-eq-equiv refl

equiv-eq-equiv : (A B : UU l) → (A ≃ B) ≃ (A ＝ B)
pr1 (equiv-eq-equiv A B) = eq-equiv
pr2 (equiv-eq-equiv A B) = is-equiv-eq-equiv A B


### The total space of all equivalences out of a type or into a type is contractible

Type families of which the total space is contractible are also called torsorial. This terminology originates from higher group theory, where a higher group action is torsorial if its type of orbits, i.e., its total space, is contractible. Our claim that the total space of all equivalences out of a type A is contractible can therefore be stated more succinctly as the claim that the family of equivalences out of A is torsorial.

module _
{l : Level}
where

abstract
is-torsorial-equiv :
(A : UU l) → is-torsorial (λ (X : UU l) → A ≃ X)
is-torsorial-equiv A =
is-torsorial-equiv-based-univalence A (univalence A)

is-torsorial-equiv' :
(A : UU l) → is-torsorial (λ (X : UU l) → X ≃ A)
is-torsorial-equiv' A =
is-contr-equiv'
( Σ (UU l) (λ X → X ＝ A))
( equiv-tot (λ X → equiv-univalence))
( is-torsorial-Id' A)


### Univalence for type families

equiv-fam :
{l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3) →
UU (l1 ⊔ l2 ⊔ l3)
equiv-fam {A = A} B C = (a : A) → B a ≃ C a

id-equiv-fam :
{l1 l2 : Level} {A : UU l1} (B : A → UU l2) → equiv-fam B B
id-equiv-fam B a = id-equiv

equiv-eq-fam :
{l1 l2 : Level} {A : UU l1} (B C : A → UU l2) → B ＝ C → equiv-fam B C
equiv-eq-fam B .B refl = id-equiv-fam B

abstract
is-torsorial-equiv-fam :
{l1 l2 : Level} {A : UU l1} (B : A → UU l2) →
is-torsorial (λ (C : A → UU l2) → equiv-fam B C)
is-torsorial-equiv-fam B =
is-torsorial-Eq-Π (λ x → is-torsorial-equiv (B x))

abstract
is-equiv-equiv-eq-fam :
{l1 l2 : Level} {A : UU l1} (B C : A → UU l2) → is-equiv (equiv-eq-fam B C)
is-equiv-equiv-eq-fam B =
fundamental-theorem-id
( is-torsorial-equiv-fam B)
( equiv-eq-fam B)

extensionality-fam :
{l1 l2 : Level} {A : UU l1} (B C : A → UU l2) → (B ＝ C) ≃ equiv-fam B C
pr1 (extensionality-fam B C) = equiv-eq-fam B C
pr2 (extensionality-fam B C) = is-equiv-equiv-eq-fam B C

eq-equiv-fam :
{l1 l2 : Level} {A : UU l1} {B C : A → UU l2} → equiv-fam B C → B ＝ C
eq-equiv-fam {B = B} {C} = map-inv-is-equiv (is-equiv-equiv-eq-fam B C)


### Computations with univalence

compute-equiv-eq-concat :
{l : Level} {A B C : UU l} (p : A ＝ B) (q : B ＝ C) →
equiv-eq q ∘e equiv-eq p ＝ equiv-eq (p ∙ q)
compute-equiv-eq-concat refl refl = eq-equiv-eq-map-equiv refl

compute-eq-equiv-comp-equiv :
{l : Level} {A B C : UU l} (f : A ≃ B) (g : B ≃ C) →
eq-equiv f ∙ eq-equiv g ＝ eq-equiv (g ∘e f)
compute-eq-equiv-comp-equiv f g =
is-injective-equiv
( equiv-univalence)
( ( inv ( compute-equiv-eq-concat (eq-equiv f) (eq-equiv g))) ∙
( ( ap
( λ e → (map-equiv e g) ∘e (equiv-eq (eq-equiv f)))
( right-inverse-law-equiv equiv-univalence)) ∙
( ( ap
( λ e → g ∘e map-equiv e f)
( right-inverse-law-equiv equiv-univalence)) ∙
( ap
( λ e → map-equiv e (g ∘e f))
( inv (right-inverse-law-equiv equiv-univalence))))))

compute-map-eq-ap-inv :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x y : A} (p : x ＝ y) →
map-eq (ap B (inv p)) ∘ map-eq (ap B p) ~ id
compute-map-eq-ap-inv refl = refl-htpy

commutativity-inv-equiv-eq :
{l : Level} {A B : UU l} (p : A ＝ B) →
inv-equiv (equiv-eq p) ＝ equiv-eq (inv p)
commutativity-inv-equiv-eq refl = eq-equiv-eq-map-equiv refl

commutativity-inv-eq-equiv :
{l : Level} {A B : UU l} (f : A ≃ B) →
inv (eq-equiv f) ＝ eq-equiv (inv-equiv f)
commutativity-inv-eq-equiv f =
is-injective-equiv
( equiv-univalence)
( ( inv (commutativity-inv-equiv-eq (eq-equiv f))) ∙
( ( ap
( λ e → (inv-equiv (map-equiv e f)))
( right-inverse-law-equiv equiv-univalence)) ∙
( ap
( λ e → map-equiv e (inv-equiv f))
( inv (right-inverse-law-equiv equiv-univalence)))))