Homotopies Properties
Table of Contents
1 Homotopies Properties
module Lib.Prop.Htpy where
This file states some properties of homotopies.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.ContrMap import Lib.FundamentalTheorem import Lib.FunExt
1.2 Equivalence property
Homotopies are reflexive;
Htpy/refl (A : U) (B : A → U) (f : (x : A) → B x) : Htpy A B f f = λx. refl (B x) (f x) Htpy'/refl (A B : U) : (f : A → B) → Htpy' A B f f = Htpy/refl A (λ_. B)
symmetric;
Htpy/sym (A : U) (B : A → U) (f g : (x : A) → B x) (H : Htpy A B f g) : Htpy A B g f = λx. inv (B x) (f x) (g x) (H x) Htpy'/sym (A B : U) : (f : A → B) → (g : A → B) → Htpy' A B f g → Htpy' A B g f = Htpy/sym A (λ_. B) Htpy/inv : (A : U) → (B : A → U) → (f g : (x : A) → B x) → (H : Htpy A B f g) → Htpy A B g f = Htpy/sym Htpy'/inv : (A B : U) → (f g : A → B) → (H : Htpy' A B f g) → Htpy' A B g f = Htpy'/sym
1.3 The total homotopy is contractible
Remark that the total space Σ (g : (x : A) → B x) (f ∼ g) is contractible iff htpy-eq is a family of equivalences by the fundamental theorem of identity types. But we know that htpy-eq is a family of equivalences, thus the result follows.
Htpy/is-contr-total-htpy (A : U) (B : A → U) (f : (x : A) → B x) : is-contr (Σ ((x : A) → B x) (λg. Htpy A B f g)) = fundamental-theorem-id' ((x : A) → B x) (λg. Htpy A B f g) f (htpy-eq A B f) (htpy-eq/is-equiv A B f)