This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
The univalence axiom
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)))))