# Pointed `2`-homotopies ```agda module structured-types.pointed-2-homotopies where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea Consider two [pointed homotopies](structured-types.pointed-homotopies.md) `H := (H₀ , H₁)` and `K := (K₀ , K₁)` between two [pointed dependent functions](structured-types.pointed-dependent-functions.md) `f := (f₀ , f₁)` and `g := (g₀ , g₁)` with base point coherences ```text H₀ * H₀ * f₀ * ------> g₀ * f₀ * ------> g₀ * \ / \ ∧ f₁ \ H₁ / g₁ and f₁ \ H̃₁ / inv g₁ \ / \ / ∨ ∨ ∨ / * * ``` and ```text K₀ * K₀ * f₀ * ------> g₀ * f₀ * ------> g₀ * \ / \ ∧ f₁ \ K₁ / g₁ and f₁ \ K̃₁ / inv g₁ \ / \ / ∨ ∨ ∨ / * *, ``` where ```text H̃₁ := coherence-triangle-inv-right f₁ g₁ (H₀ *) H₁ K̃₁ := coherence-triangle-inv-right f₁ g₁ (K₀ *) K₁ ``` A {{#concept "pointed `2`-homotopy" Agda=_~²∗_}} `H ~²∗ K` then consists of an unpointed [homotopy](foundation-core.homotopies.md) `α₀ : H₀ ~ K₀` and an [identification](foundation-core.identity-types.md) witnessing that the triangle ```text H₁ f₁ ------> (H₀ *) ∙ g₁ \ / K₁ \ / right-whisker-concat (α₀ *) g₁ \ / ∨ ∨ (K₀ *) ∙ g₁ ``` [commutes](foundation.commuting-triangles-of-identifications.md). Equivalently, following the [equivalence](foundation-core.equivalences.md) of pointed homotopies and [uniform pointed homotopies](structured-types.uniform-pointed-homotopies.md), 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 ```text α₀ * 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. ```agda 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 ```agda 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 ```text (α ∙h β)₀ := α₀ ∙h β₀. ``` The base point coherence `(α ∙h β)₁` is an identification witnessing that the triangle ```text 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 ```text 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. ```agda 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 ```agda 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. ```agda 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 ```agda 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 ```text (G ∙h H) ∙h K ~²∗ G ∙h (H ∙h K). ``` ```agda 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 ```text refl-pointed-htpy ∙h H ~²∗ H. ``` ```agda 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 ```text 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 ```text (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 ```text 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. ```agda 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 ```