Equivalence induction
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-15.
Last modified on 2023-09-15.
module foundation.equivalence-induction where
Imports
open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.identity-systems open import foundation.subuniverses open import foundation.univalence open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels open import foundation-core.commuting-triangles-of-maps open import foundation-core.contractible-maps open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.sections open import foundation-core.singleton-induction
Idea
Equivalence induction is the principle asserting that for any type family
P : (B : 𝒰) (e : A ≃ B) → 𝒰
of types indexed by all equivalences with domain
A
, there is a section of the evaluation map
((B : 𝒰) (e : A ≃ B) → P B e) → P A id-equiv.
The principle of equivalence induction is equivalent to the univalence axiom.
By equivalence induction, it follows that any type family P : 𝒰 → 𝒱
on the
universe has an
action on equivalences
(A ≃ B) → P A ≃ P B.
Statement
module _ {l1 : Level} {A : UU l1} where ev-id-equiv : {l : Level} (P : (B : UU l1) → (A ≃ B) → UU l) → ((B : UU l1) (e : A ≃ B) → P B e) → P A id-equiv ev-id-equiv P f = f A id-equiv induction-principle-equivalences : {l : Level} (P : (B : UU l1) (e : A ≃ B) → UU l) → UU (lsuc l1 ⊔ l) induction-principle-equivalences P = section (ev-id-equiv P) triangle-ev-id-equiv : {l : Level} (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → coherence-triangle-maps ( ev-point (A , id-equiv) {P}) ( ev-id-equiv (λ X e → P (X , e))) ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P}) triangle-ev-id-equiv P f = refl
Properties
Equivalence induction is equivalent to the contractibility of the total space of equivalences
Contractibility of the total space of equivalences implies equivalence induction
module _ {l1 : Level} {A : UU l1} where abstract is-identity-system-is-contr-total-equiv : is-contr (Σ (UU l1) (λ X → A ≃ X)) → {l : Level} → (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → induction-principle-equivalences (λ B e → P (B , e)) is-identity-system-is-contr-total-equiv c P = section-left-factor ( ev-id-equiv (λ X e → P (X , e))) ( ev-pair) ( is-singleton-is-contr ( A , id-equiv) ( ( A , id-equiv) , ( λ t → ( inv (contraction c (A , id-equiv))) ∙ (contraction c t))) ( P))
Equivalence induction implies contractibility of the total space of equivalences
module _ {l1 : Level} {A : UU l1} where abstract is-contr-total-is-identity-system-equiv : ( {l : Level} → is-identity-system l (λ X → A ≃ X) A id-equiv) → is-contr (Σ (UU l1) (λ X → A ≃ X)) is-contr-total-is-identity-system-equiv ind = is-contr-is-singleton ( Σ (UU l1) (λ X → A ≃ X)) ( A , id-equiv) ( λ P → section-comp ( ev-id-equiv (λ X e → P (X , e))) ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P}) ( ind-Σ , refl-htpy) ( ind (λ X e → P (X , e))))
Equivalence induction in a universe
module _ {l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2) where abstract is-identity-system-equiv : section (ev-id-equiv P) is-identity-system-equiv = is-identity-system-is-contr-total-equiv ( is-contr-total-equiv _) ( λ t → P (pr1 t) (pr2 t)) ind-equiv : P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e ind-equiv p {B} = pr1 is-identity-system-equiv p B compute-ind-equiv : (u : P A id-equiv) → ind-equiv u id-equiv = u compute-ind-equiv = pr2 is-identity-system-equiv
Equivalence induction in a subuniverse
module _ {l1 l2 l3 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) where ev-id-equiv-subuniverse : {F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3} → ((B : type-subuniverse P) (e : equiv-subuniverse P A B) → F B e) → F A id-equiv ev-id-equiv-subuniverse f = f A id-equiv triangle-ev-id-equiv-subuniverse : (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → coherence-triangle-maps ( ev-point (A , id-equiv)) ( ev-id-equiv-subuniverse {F}) ( ev-pair) triangle-ev-id-equiv-subuniverse F E = refl abstract is-identity-system-equiv-subuniverse : (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → section (ev-id-equiv-subuniverse {F}) is-identity-system-equiv-subuniverse = is-identity-system-is-torsorial A id-equiv ( is-contr-total-equiv-subuniverse P A) ind-equiv-subuniverse : (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → F A id-equiv → (B : type-subuniverse P) (e : equiv-subuniverse P A B) → F B e ind-equiv-subuniverse F = pr1 (is-identity-system-equiv-subuniverse F) compute-ind-equiv-subuniverse : (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) → (u : F A id-equiv) → ind-equiv-subuniverse F u A id-equiv = u compute-ind-equiv-subuniverse F = pr2 (is-identity-system-equiv-subuniverse F)
The evaluation map ev-id-equiv
is an equivalence
module _ {l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2) where is-equiv-ev-id-equiv : is-equiv (ev-id-equiv P) is-equiv-ev-id-equiv = is-equiv-left-factor-htpy ( ev-point (A , id-equiv)) ( ev-id-equiv P) ( ev-pair) ( triangle-ev-id-equiv (λ u → P (pr1 u) (pr2 u))) ( dependent-universal-property-contr-is-contr ( A , id-equiv) ( is-contr-total-equiv A) ( λ u → P (pr1 u) (pr2 u))) ( is-equiv-ev-pair) is-contr-map-ev-id-equiv : is-contr-map (ev-id-equiv P) is-contr-map-ev-id-equiv = is-contr-map-is-equiv is-equiv-ev-id-equiv
The evaluation map ev-id-equiv-subuniverse
is an equivalence
module _ {l1 l2 l3 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P) (F : (Y : type-subuniverse P) (e : equiv-subuniverse P X Y) → UU l3) where is-equiv-ev-id-equiv-subuniverse : is-equiv (ev-id-equiv-subuniverse P X {F}) is-equiv-ev-id-equiv-subuniverse = is-equiv-left-factor-htpy ( ev-point (X , id-equiv)) ( ev-id-equiv-subuniverse P X) ( ev-pair) ( triangle-ev-id-equiv-subuniverse P X F) ( dependent-universal-property-contr-is-contr ( X , id-equiv) ( is-contr-total-equiv-subuniverse P X) ( λ E → F (pr1 E) (pr2 E))) ( is-equiv-ev-pair) is-contr-map-ev-id-equiv-subuniverse : is-contr-map (ev-id-equiv-subuniverse P X {F}) is-contr-map-ev-id-equiv-subuniverse = is-contr-map-is-equiv is-equiv-ev-id-equiv-subuniverse
Equivalence induction implies that postcomposing by an equivalence is an equivalence
Of course we already know that this fact follows from function extensionality. However, we prove it again from equivalence induction so that we can prove that univalence implies function extensionality.
abstract is-equiv-postcomp-univalence : {l1 l2 : Level} {X Y : UU l1} (A : UU l2) (e : X ≃ Y) → is-equiv (postcomp A (map-equiv e)) is-equiv-postcomp-univalence {X = X} A = ind-equiv (λ Y e → is-equiv (postcomp A (map-equiv e))) is-equiv-id
Recent changes
- 2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).