Pointed 2-homotopies
Content created by Egbert Rijke.
Created on 2024-03-13.
Last modified on 2024-03-13.
module structured-types.pointed-2-homotopies where
Imports
open import foundation.action-on-identifications-functions open import foundation.binary-equivalences open import foundation.commuting-triangles-of-identifications open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.homotopy-induction open import foundation.identity-types open import foundation.path-algebra open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.universe-levels open import foundation.whiskering-identifications-concatenation open import structured-types.pointed-dependent-functions open import structured-types.pointed-families-of-types open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-types open import structured-types.uniform-pointed-homotopies
Idea
Consider two pointed homotopies
H := (H₀ , H₁) and K := (K₀ , K₁) between two
pointed dependent functions
f := (f₀ , f₁) and g := (g₀ , g₁) with base point coherences
H₀ * H₀ *
f₀ * ------> g₀ * f₀ * ------> g₀ *
\ / \ ∧
f₁ \ H₁ / g₁ and f₁ \ H̃₁ / inv g₁
\ / \ /
∨ ∨ ∨ /
* *
and
K₀ * K₀ *
f₀ * ------> g₀ * f₀ * ------> g₀ *
\ / \ ∧
f₁ \ K₁ / g₁ and f₁ \ K̃₁ / inv g₁
\ / \ /
∨ ∨ ∨ /
* *,
where
H̃₁ := coherence-triangle-inv-right f₁ g₁ (H₀ *) H₁
K̃₁ := coherence-triangle-inv-right f₁ g₁ (K₀ *) K₁
A pointed 2-homotopy¶ H ~²∗ K then consists of an
unpointed homotopy α₀ : H₀ ~ K₀ and an
identification witnessing that the triangle
H₁
f₁ ------> (H₀ *) ∙ g₁
\ /
K₁ \ / right-whisker-concat (α₀ *) g₁
\ /
∨ ∨
(K₀ *) ∙ g₁
commutes. Equivalently,
following the equivalence of pointed
homotopies and
uniform pointed homotopies, a
uniform pointed 2-homotopy consists of an unpointed homotopy α₀ : H₀ ~ K₀
and an identification witnessing that α₀ preserves the base point, i.e.,
witnessing that the triangle
α₀ *
H₀ * ------> K₀ *
\ ∧
H̃₁ \ / inv K̃₁
\ /
∨ /
f₁ ∙ inv g₁
commutes. Note that such identifications are often much harder to construct. Our
preferred definition of pointed 2-homotopies is therefore the non-uniform
definition described first.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} (H K : pointed-htpy f g) where unpointed-htpy-pointed-htpy : UU (l1 ⊔ l2) unpointed-htpy-pointed-htpy = htpy-pointed-htpy H ~ htpy-pointed-htpy K coherence-point-unpointed-htpy-pointed-htpy : unpointed-htpy-pointed-htpy → UU l2 coherence-point-unpointed-htpy-pointed-htpy α = coherence-triangle-identifications ( coherence-point-pointed-htpy K) ( right-whisker-concat ( α (point-Pointed-Type A)) ( preserves-point-function-pointed-Π g)) ( coherence-point-pointed-htpy H) pointed-2-htpy : UU (l1 ⊔ l2) pointed-2-htpy = Σ unpointed-htpy-pointed-htpy coherence-point-unpointed-htpy-pointed-htpy infix 6 _~²∗_ _~²∗_ : UU (l1 ⊔ l2) _~²∗_ = pointed-2-htpy module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} {H K : pointed-htpy f g} (α : pointed-2-htpy H K) where htpy-pointed-2-htpy : unpointed-htpy-pointed-htpy H K htpy-pointed-2-htpy = pr1 α coherence-point-pointed-2-htpy : coherence-point-unpointed-htpy-pointed-htpy H K htpy-pointed-2-htpy coherence-point-pointed-2-htpy = pr2 α preserves-point-pointed-2-htpy : preserves-point-unpointed-htpy-pointed-Π ( make-uniform-pointed-htpy ( htpy-pointed-htpy H) ( coherence-point-pointed-htpy H)) ( make-uniform-pointed-htpy ( htpy-pointed-htpy K) ( coherence-point-pointed-htpy K)) ( htpy-pointed-2-htpy) preserves-point-pointed-2-htpy = transpose-right-coherence-triangle-identifications ( htpy-pointed-2-htpy (point-Pointed-Type A)) ( preserves-point-pointed-htpy K) ( preserves-point-pointed-htpy H) ( refl) ( higher-transpose-right-coherence-triangle-identifications ( htpy-pointed-htpy H (point-Pointed-Type A)) ( preserves-point-function-pointed-Π g) ( preserves-point-function-pointed-Π f) ( htpy-pointed-2-htpy (point-Pointed-Type A)) ( refl) ( coherence-point-pointed-htpy H) ( coherence-point-pointed-htpy K) ( coherence-point-pointed-2-htpy)) uniform-pointed-htpy-pointed-2-htpy : uniform-pointed-htpy ( uniform-pointed-htpy-pointed-htpy H) ( uniform-pointed-htpy-pointed-htpy K) pr1 uniform-pointed-htpy-pointed-2-htpy = htpy-pointed-2-htpy pr2 uniform-pointed-htpy-pointed-2-htpy = preserves-point-pointed-2-htpy
The reflexive pointed 2-homotopy
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} (H : f ~∗ g) where htpy-refl-pointed-2-htpy : unpointed-htpy-pointed-htpy H H htpy-refl-pointed-2-htpy = refl-htpy coherence-point-refl-pointed-2-htpy : coherence-point-unpointed-htpy-pointed-htpy H H ( htpy-refl-pointed-2-htpy) coherence-point-refl-pointed-2-htpy = inv right-unit refl-pointed-2-htpy : H ~²∗ H pr1 refl-pointed-2-htpy = htpy-refl-pointed-2-htpy pr2 refl-pointed-2-htpy = coherence-point-refl-pointed-2-htpy
Concatenation of pointed 2-homotopies
Consider two pointed dependent functions f := (f₀ , f₁) and g := (g₀ , g₁)
and three pointed homotopies H := (H₀ , H₁), K := (K₀ , K₁), and
L := (L₀ , L₁) between them. Furthermore, consider two pointed 2-homotopies
α := (α₀ , α₁) : H ~²∗ K and β := (β₀ , β₁) : K ~²∗ L. The underlying
homotopy of the concatenation α ∙h β is simply the concatenation of homotopies
(α ∙h β)₀ := α₀ ∙h β₀.
The base point coherence (α ∙h β)₁ is an identification witnessing that the
triangle
H₁
f₁ ------> (H₀ *) ∙ h₁
\ /
L₁ \ / right-whisker-concat ((α₀ *) ∙h (β₀ *)) g₁
\ /
∨ ∨
(L₀ *) ∙ h₁
commutes. Note that right whiskering of identifications with respect to concatenation distributes over concatenation. The identification witnessing the commutativity of the above triangle can therefore be constructed by constructing an identification witnessing that the triangle
H₁
f₁ ----------> (H₀ *) ∙ h₁
\ /
\ / right-whisker-concat (α₀ *) g₁
\ ∨
L₁ \ (K₀ *) ∙ h₁
\ /
\ / right-whisker-concat (β₀ *) g₁
∨ ∨
(L₀ *) ∙ h₁
commutes. This triangle commutes by right pasting of commuting triangles of identifications.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} {H K L : f ~∗ g} (α : H ~²∗ K) (β : K ~²∗ L) where htpy-concat-pointed-2-htpy : unpointed-htpy-pointed-htpy H L htpy-concat-pointed-2-htpy = htpy-pointed-2-htpy α ∙h htpy-pointed-2-htpy β coherence-point-concat-pointed-2-htpy : coherence-point-unpointed-htpy-pointed-htpy H L htpy-concat-pointed-2-htpy coherence-point-concat-pointed-2-htpy = ( right-pasting-coherence-triangle-identifications _ _ _ _ ( coherence-point-pointed-htpy H) ( coherence-point-pointed-2-htpy β) ( coherence-point-pointed-2-htpy α)) ∙ ( inv ( left-whisker-concat ( coherence-point-pointed-htpy H) ( distributive-right-whisker-concat-concat ( htpy-pointed-2-htpy α _) ( htpy-pointed-2-htpy β _) ( preserves-point-function-pointed-Π g)))) concat-pointed-2-htpy : H ~²∗ L pr1 concat-pointed-2-htpy = htpy-concat-pointed-2-htpy pr2 concat-pointed-2-htpy = coherence-point-concat-pointed-2-htpy
Inverses of pointed 2-homotopies
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} {H K : f ~∗ g} (α : H ~²∗ K) where htpy-inv-pointed-2-htpy : unpointed-htpy-pointed-htpy K H htpy-inv-pointed-2-htpy = inv-htpy (htpy-pointed-2-htpy α) coherence-point-inv-pointed-2-htpy : coherence-point-unpointed-htpy-pointed-htpy K H htpy-inv-pointed-2-htpy coherence-point-inv-pointed-2-htpy = transpose-right-coherence-triangle-identifications ( coherence-point-pointed-htpy H) ( right-whisker-concat (htpy-pointed-2-htpy α _) _) ( coherence-point-pointed-htpy K) ( inv (ap-inv _ (htpy-pointed-2-htpy α _))) ( coherence-point-pointed-2-htpy α) inv-pointed-2-htpy : K ~²∗ H pr1 inv-pointed-2-htpy = htpy-inv-pointed-2-htpy pr2 inv-pointed-2-htpy = coherence-point-inv-pointed-2-htpy
Properties
Extensionality of pointed homotopies
Pointed 2-homotopies characterize identifications of pointed homotopies.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} (H : f ~∗ g) where is-torsorial-pointed-2-htpy : is-torsorial (pointed-2-htpy H) is-torsorial-pointed-2-htpy = is-torsorial-Eq-structure ( is-torsorial-htpy _) ( htpy-pointed-htpy H , refl-htpy) ( is-torsorial-Id' _) pointed-2-htpy-eq : (K : f ~∗ g) → H ＝ K → H ~²∗ K pointed-2-htpy-eq .H refl = refl-pointed-2-htpy H is-equiv-pointed-2-htpy-eq : (K : f ~∗ g) → is-equiv (pointed-2-htpy-eq K) is-equiv-pointed-2-htpy-eq = fundamental-theorem-id ( is-torsorial-pointed-2-htpy) ( pointed-2-htpy-eq) extensionality-pointed-htpy : (K : f ~∗ g) → (H ＝ K) ≃ (H ~²∗ K) pr1 (extensionality-pointed-htpy K) = pointed-2-htpy-eq K pr2 (extensionality-pointed-htpy K) = is-equiv-pointed-2-htpy-eq K eq-pointed-2-htpy : (K : f ~∗ g) → H ~²∗ K → H ＝ K eq-pointed-2-htpy K = map-inv-equiv (extensionality-pointed-htpy K)
Concatenation of pointed 2-homotopies is a binary equivalence
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} {H K L : f ~∗ g} where abstract is-equiv-concat-pointed-2-htpy : (α : H ~²∗ K) → is-equiv (λ (β : K ~²∗ L) → concat-pointed-2-htpy α β) is-equiv-concat-pointed-2-htpy α = is-equiv-map-Σ _ ( is-equiv-concat-htpy (htpy-pointed-2-htpy α) _) ( λ β → is-equiv-comp _ _ ( is-equiv-right-pasting-coherence-triangle-identifications' ( coherence-point-pointed-htpy L) ( right-whisker-concat ( htpy-pointed-2-htpy α _) ( preserves-point-function-pointed-Π g)) ( right-whisker-concat ( β _) ( preserves-point-function-pointed-Π g)) ( coherence-point-pointed-htpy K) ( coherence-point-pointed-htpy H) ( coherence-point-pointed-2-htpy α)) ( is-equiv-concat' _ ( inv ( left-whisker-concat ( coherence-point-pointed-htpy H) ( distributive-right-whisker-concat-concat ( htpy-pointed-2-htpy α _) ( β _) ( preserves-point-function-pointed-Π g)))))) equiv-concat-pointed-2-htpy : H ~²∗ K → (K ~²∗ L) ≃ (H ~²∗ L) pr1 (equiv-concat-pointed-2-htpy α) = concat-pointed-2-htpy α pr2 (equiv-concat-pointed-2-htpy α) = is-equiv-concat-pointed-2-htpy α abstract is-equiv-concat-pointed-2-htpy' : (β : K ~²∗ L) → is-equiv (λ (α : H ~²∗ K) → concat-pointed-2-htpy α β) is-equiv-concat-pointed-2-htpy' β = is-equiv-map-Σ _ ( is-equiv-concat-htpy' _ (htpy-pointed-2-htpy β)) ( λ α → is-equiv-comp _ _ ( is-equiv-right-pasting-coherence-triangle-identifications ( coherence-point-pointed-htpy L) ( right-whisker-concat ( α _) ( preserves-point-function-pointed-Π g)) ( right-whisker-concat ( htpy-pointed-2-htpy β _) ( preserves-point-function-pointed-Π g)) ( coherence-point-pointed-htpy K) ( coherence-point-pointed-htpy H) ( coherence-point-pointed-2-htpy β)) ( is-equiv-concat' _ ( inv ( left-whisker-concat ( coherence-point-pointed-htpy H) ( distributive-right-whisker-concat-concat ( α _) ( htpy-pointed-2-htpy β _) ( preserves-point-function-pointed-Π g)))))) equiv-concat-pointed-2-htpy' : K ~²∗ L → (H ~²∗ K) ≃ (H ~²∗ L) pr1 (equiv-concat-pointed-2-htpy' β) α = concat-pointed-2-htpy α β pr2 (equiv-concat-pointed-2-htpy' β) = is-equiv-concat-pointed-2-htpy' β is-binary-equiv-concat-pointed-2-htpy : is-binary-equiv (λ (α : H ~²∗ K) (β : K ~²∗ L) → concat-pointed-2-htpy α β) pr1 is-binary-equiv-concat-pointed-2-htpy = is-equiv-concat-pointed-2-htpy' pr2 is-binary-equiv-concat-pointed-2-htpy = is-equiv-concat-pointed-2-htpy
Associativity of concatenation of pointed homotopies
Associativity of concatenation of three pointed homotopies G, H, and K is
a pointed 2-homotopy
(G ∙h H) ∙h K ~²∗ G ∙h (H ∙h K).
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g h k : pointed-Π A B} (G : f ~∗ g) (H : g ~∗ h) (K : h ~∗ k) where htpy-associative-concat-pointed-htpy : htpy-pointed-htpy ( concat-pointed-htpy (concat-pointed-htpy G H) K) ~ htpy-pointed-htpy ( concat-pointed-htpy G (concat-pointed-htpy H K)) htpy-associative-concat-pointed-htpy = assoc-htpy ( htpy-pointed-htpy G) ( htpy-pointed-htpy H) ( htpy-pointed-htpy K) coherence-associative-concat-pointed-htpy : coherence-point-unpointed-htpy-pointed-htpy ( concat-pointed-htpy (concat-pointed-htpy G H) K) ( concat-pointed-htpy G (concat-pointed-htpy H K)) ( htpy-associative-concat-pointed-htpy) coherence-associative-concat-pointed-htpy = associative-horizontal-pasting-coherence-triangle-identifications ( preserves-point-function-pointed-Π f) ( preserves-point-function-pointed-Π g) ( preserves-point-function-pointed-Π h) ( preserves-point-function-pointed-Π k) ( htpy-pointed-htpy G _) ( htpy-pointed-htpy H _) ( htpy-pointed-htpy K _) ( coherence-point-pointed-htpy G) ( coherence-point-pointed-htpy H) ( coherence-point-pointed-htpy K) associative-concat-pointed-htpy : concat-pointed-htpy (concat-pointed-htpy G H) K ~²∗ concat-pointed-htpy G (concat-pointed-htpy H K) pr1 associative-concat-pointed-htpy = htpy-associative-concat-pointed-htpy pr2 associative-concat-pointed-htpy = coherence-associative-concat-pointed-htpy
The left unit law of concatenation of pointed homotopies
Consider a pointed homotopy H := (H₀ , H₁) between pointed dependent functions
f := (f₀ , f₁) and g := (g₀ , g₁). Then there is a pointed 2-homotopy of
type
refl-pointed-htpy ∙h H ~²∗ H.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} (H : f ~∗ g) where htpy-left-unit-law-concat-pointed-htpy : unpointed-htpy-pointed-htpy ( concat-pointed-htpy (refl-pointed-htpy f) H) ( H) htpy-left-unit-law-concat-pointed-htpy = refl-htpy coherence-point-left-unit-law-concat-pointed-htpy : coherence-point-unpointed-htpy-pointed-htpy ( concat-pointed-htpy (refl-pointed-htpy f) H) ( H) ( htpy-left-unit-law-concat-pointed-htpy) coherence-point-left-unit-law-concat-pointed-htpy = inv (right-unit ∙ right-unit ∙ ap-id (coherence-point-pointed-htpy H)) left-unit-law-concat-pointed-htpy : concat-pointed-htpy (refl-pointed-htpy f) H ~²∗ H pr1 left-unit-law-concat-pointed-htpy = htpy-left-unit-law-concat-pointed-htpy pr2 left-unit-law-concat-pointed-htpy = coherence-point-left-unit-law-concat-pointed-htpy
The right unit law of concatenation of pointed homotopies
Consider a pointed homotopy H := (H₀ , H₁) between pointed dependent functions
f := (f₀ , f₁) and g := (g₀ , g₁). Then there is a pointed 2-homotopy
H ∙h refl-pointed-htpy ~²∗ H.
The underlying homotopy of this pointed 2-homotopy is the homotopy
right-unit-htpy. The base point coherence of this homotopy is an
identification witnessing that the triangle
(H ∙h refl)₁
f₁ ------------> (H₀ * ∙ refl) ∙ g₁
\ /
H₁ \ / right-whisker-concat right-unit g₁
\ /
∨ ∨
(H₀ *) ∙ g₁
commutes. Here, the identification (H ∙h refl)₁ is the horizontal pasting of
commuting triangles of identifications
H₀ * refl
f₀ * --> g₀ * ---> g₀ *
\ | /
\ | g₁ /
f₁ \ | / g₁
\ | /
\ | /
∨ ∨ ∨
*.
The upper triangle therefore commutes by the right unit law of horizontal pasting of commuting triangles of identifications.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g : pointed-Π A B} (H : f ~∗ g) where htpy-right-unit-law-concat-pointed-htpy : unpointed-htpy-pointed-htpy ( concat-pointed-htpy H (refl-pointed-htpy g)) ( H) htpy-right-unit-law-concat-pointed-htpy = right-unit-htpy coherence-point-right-unit-law-concat-pointed-htpy : coherence-point-unpointed-htpy-pointed-htpy ( concat-pointed-htpy H (refl-pointed-htpy g)) ( H) ( htpy-right-unit-law-concat-pointed-htpy) coherence-point-right-unit-law-concat-pointed-htpy = right-unit-law-horizontal-pasting-coherence-triangle-identifications ( preserves-point-function-pointed-Π f) ( preserves-point-function-pointed-Π g) ( htpy-pointed-htpy H _) ( coherence-point-pointed-htpy H) right-unit-law-concat-pointed-htpy : concat-pointed-htpy H (refl-pointed-htpy g) ~²∗ H pr1 right-unit-law-concat-pointed-htpy = htpy-right-unit-law-concat-pointed-htpy pr2 right-unit-law-concat-pointed-htpy = coherence-point-right-unit-law-concat-pointed-htpy
Recent changes
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).