# The univalence axiom

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

Created on 2022-02-15.

module foundation-core.univalence where

Imports
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


## 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 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.

## Definitions

### Equalities induce equivalences

module _
{l : Level}
where

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


## Properties

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

abstract
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

abstract
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

                 equiv-eq
(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}
where

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)