Homotopy induction
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2022-01-31.
Last modified on 2023-10-22.
module foundation.homotopy-induction where
Imports
open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.identity-systems open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.torsorial-type-families
Idea
The principle of homotopy induction asserts that homotopies form an identity system on dependent function types.
Statement
ev-refl-htpy : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) (C : (g : (x : A) → B x) → f ~ g → UU l3) → ((g : (x : A) → B x) (H : f ~ g) → C g H) → C f refl-htpy ev-refl-htpy f C φ = φ f refl-htpy induction-principle-homotopies : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) → UUω induction-principle-homotopies f = is-identity-system (f ~_) f (refl-htpy)
Propositions
The total space of homotopies 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
homotopies from a function f
is contractible can therefore be stated more
succinctly as the claim that the family of homotopies from f
is torsorial.
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) where abstract is-torsorial-htpy : is-torsorial (λ g → f ~ g) is-torsorial-htpy = is-contr-equiv' ( Σ ((x : A) → B x) (Id f)) ( equiv-tot (λ g → equiv-funext)) ( is-torsorial-path f) abstract is-torsorial-htpy' : is-torsorial (λ g → g ~ f) is-torsorial-htpy' = is-contr-equiv' ( Σ ((x : A) → B x) (λ g → g = f)) ( equiv-tot (λ g → equiv-funext)) ( is-torsorial-path' f)
Homotopy induction is equivalent to function extensionality
abstract induction-principle-homotopies-based-function-extensionality : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) → based-function-extensionality f → induction-principle-homotopies f induction-principle-homotopies-based-function-extensionality {A = A} {B} f funext-f = is-identity-system-is-torsorial f ( refl-htpy) ( is-torsorial-htpy f) abstract based-function-extensionality-induction-principle-homotopies : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) → induction-principle-homotopies f → based-function-extensionality f based-function-extensionality-induction-principle-homotopies f ind-htpy-f = fundamental-theorem-id-is-identity-system f ( refl-htpy) ( ind-htpy-f) ( λ _ → htpy-eq)
Homotopy induction
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where abstract induction-principle-htpy : (f : (x : A) → B x) → induction-principle-homotopies f induction-principle-htpy f = induction-principle-homotopies-based-function-extensionality f (funext f) ind-htpy : {l3 : Level} (f : (x : A) → B x) (C : (g : (x : A) → B x) → f ~ g → UU l3) → C f refl-htpy → {g : (x : A) → B x} (H : f ~ g) → C g H ind-htpy f C t {g} = pr1 (induction-principle-htpy f C) t g compute-ind-htpy : {l3 : Level} (f : (x : A) → B x) (C : (g : (x : A) → B x) → f ~ g → UU l3) → (c : C f refl-htpy) → ind-htpy f C c refl-htpy = c compute-ind-htpy f C = pr2 (induction-principle-htpy f C)
See also
Recent changes
- 2023-10-22. Egbert Rijke and Fredrik Bakke. Refactor synthetic homotopy theory (#654).
- 2023-10-22. Fredrik Bakke. Refactor funext (#878).
- 2023-10-21. Egbert Rijke and Fredrik Bakke. Implement
is-torsorial
throughout the library (#875). - 2023-10-21. Egbert Rijke. Rename
is-contr-total
tois-torsorial
(#871). - 2023-09-15. Egbert Rijke. update contributors, remove unused imports (#772).