The univalence axiom
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-15.
Last modified on 2023-09-11.
module foundation-core.univalence where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.transport-along-identifications
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 map-eq : {l : Level} {A : UU l} {B : UU l} → A = B → A → B map-eq = map-equiv ∘ equiv-eq 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
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-08-23. Fredrik Bakke. Pre-commit fixes and some miscellaneous changes (#705).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).