# Whiskering of pointed homotopies with respect to composition of pointed maps ```agda module structured-types.whiskering-pointed-homotopies-composition where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications open import foundation.commuting-triangles-of-identifications open import foundation.dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation.whiskering-identifications-concatenation open import structured-types.pointed-2-homotopies 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 ``` </details> ## Idea The [whiskering operations](foundation.whiskering-operations.md) of [pointed homotopies](structured-types.pointed-homotopies.md) with respect to composition of [pointed maps](structured-types.pointed-maps.md) are two operations that produce pointed homotopies between composites of pointed maps from either a pointed homotopy on the left or on the right of the composition. - Consider a pointed homotopy `H : f ~∗ g` between pointed maps `f g : A →∗ B`, and consider a pointed map `h : B →∗ C`, as indicated in the diagram ```text f -----> h A -----> B -----> C. g ``` The {{#concept "left whiskering operation on pointed homotopies" Agda=left-whisker-comp-pointed-htpy}} of `h` and `H` is a pointed homotopy ```text h ·l∗ H : h ∘∗ f ~∗ h ∘∗ g. ``` - Consider a pointed map `f : A →∗ B` and consider a pointed homotopy `H : g ~∗ g` between tw pointed maps `g h : B →∗ C`, as indicated in the diagram ```text g f -----> A -----> B -----> C. h ``` The {{#concept "right whiskering operation on pointed homotopies" Agda=right-whisker-comp-pointed-htpy}} of `H` and `f` is a pointed homotopy ```text H ·r∗ f : g ∘∗ f ~∗ h ∘∗ f. ``` ## Definitions ### Left whiskering of pointed homotopies Consider two pointed maps `f := (f₀ , f₁) : A →∗ B` and `g := (g₀ , g₁) : A →∗ B` equipped with a pointed homotopy `H := (H₀ , H₁) : f ~∗ g`, and consider furthermore a pointed map `h := (h₀ , h₁) : B →∗ C`. Then we construct a pointed homotopy ```text h ·l∗ H : (h ∘∗ f) ~∗ (h ∘∗ g). ``` **Construction.** The underlying homotopy of `h ·l∗ H` is the whiskered homotpy ```text h₀ ·l H₀. ``` For the coherence, we have to show that the triangle ```text ap h₀ (H₀ *) h₀ (f₀ *) ------------> h₀ (g₀ *) \ / ap h₀ f₁ \ / ap h₀ g₁ ∨ ∨ h₀ * h₀ * \ / h₁ \ / h₁ ∨ ∨ ∗ ``` commutes. By right whiskering of [commuting triangles of identifications](foundation.commuting-squares-of-identifications.md) with respect to concatenation it suffices to show that the triangle ```text ap h₀ (H₀ *) h₀ (f₀ *) ---------> h₀ (g₀ *) \ / ap h₀ f₁ \ / ap h₀ g₁ \ / ∨ ∨ h₀ * ``` commutes. By functoriality of commuting triangles of identifications, this follows from the fact that the triangle ```text H₀ * f₀ * ------> g₀ * \ / f₁ \ / g₁ \ / ∨ ∨ * ``` commutes. ```agda module _ {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} (h : B →∗ C) (f g : A →∗ B) (H : f ~∗ g) where htpy-left-whisker-comp-pointed-htpy : map-comp-pointed-map h f ~ map-comp-pointed-map h g htpy-left-whisker-comp-pointed-htpy = map-pointed-map h ·l htpy-pointed-htpy H coherence-point-left-whisker-comp-pointed-htpy : coherence-point-unpointed-htpy-pointed-Π ( h ∘∗ f) ( h ∘∗ g) ( htpy-left-whisker-comp-pointed-htpy) coherence-point-left-whisker-comp-pointed-htpy = right-whisker-concat-coherence-triangle-identifications ( ap (map-pointed-map h) (preserves-point-pointed-map f)) ( ap (map-pointed-map h) (preserves-point-pointed-map g)) ( ap ( map-pointed-map h) ( htpy-pointed-htpy H (point-Pointed-Type A))) ( preserves-point-pointed-map h) ( map-coherence-triangle-identifications ( map-pointed-map h) ( preserves-point-pointed-map f) ( preserves-point-pointed-map g) ( htpy-pointed-htpy H (point-Pointed-Type A)) ( coherence-point-pointed-htpy H)) left-whisker-comp-pointed-htpy : h ∘∗ f ~∗ h ∘∗ g pr1 left-whisker-comp-pointed-htpy = htpy-left-whisker-comp-pointed-htpy pr2 left-whisker-comp-pointed-htpy = coherence-point-left-whisker-comp-pointed-htpy ``` ### Right whiskering of pointed homotopies Consider a pointed map `f := (f₀ , f₁) : A →∗ B` and two pointed maps `g := (g₀ , g₁) : B →∗ C` and `h := (h₀ , h₁) : B →∗ C` equipped with a pointed homotopy `H := (H₀ , H₁) : g ~∗ h`. Then we construct a pointed homotopy ```text H ·r∗ f : (g ∘∗ f) ~∗ (h ∘∗ f). ``` **Construction.** The underlying homotopy of `H ·r∗ f` is the homotopy ```text H₀ ·r f₀ : (g₀ ∘ f₀) ~ (h₀ ∘ f₀). ``` Then we have to show that the outer triangle in the diagram ```text H₀ (f₀ *) g₀ (f₀ *) ------------> h₀ (f₀ *) \ / ap g₀ f₁ \ / ap h₀ f₁ ∨ H₀ * ∨ g₀ * ----> h₀ * \ / g₁ \ / h₁ ∨ ∨ ∗ ``` commutes. This is done by vertically pasting the upper square and the lower triangle. The upper square commutes by inverse naturality of the homotopy `H₀`. The lower triangle is the base point coherence `H₁` of the pointed homotopy `H ≐ (H₀ , H₁)`. ```agda module _ {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} (g1 g2 : B →∗ C) (H : g1 ~∗ g2) (f : A →∗ B) where htpy-right-whisker-comp-pointed-htpy : unpointed-htpy-pointed-Π (g1 ∘∗ f) (g2 ∘∗ f) htpy-right-whisker-comp-pointed-htpy = htpy-pointed-htpy H ·r map-pointed-map f coherence-point-right-whisker-comp-pointed-htpy : coherence-point-unpointed-htpy-pointed-Π ( g1 ∘∗ f) ( g2 ∘∗ f) ( htpy-right-whisker-comp-pointed-htpy) coherence-point-right-whisker-comp-pointed-htpy = vertical-pasting-coherence-square-coherence-triangle-identifications ( htpy-pointed-htpy H _) ( ap (map-pointed-map g1) _) ( ap (map-pointed-map g2) _) ( htpy-pointed-htpy H _) ( preserves-point-pointed-map g1) ( preserves-point-pointed-map g2) ( inv-nat-htpy (htpy-pointed-htpy H) _) ( coherence-point-pointed-htpy H) right-whisker-comp-pointed-htpy : g1 ∘∗ f ~∗ g2 ∘∗ f pr1 right-whisker-comp-pointed-htpy = htpy-right-whisker-comp-pointed-htpy pr2 right-whisker-comp-pointed-htpy = coherence-point-right-whisker-comp-pointed-htpy ``` ## Properties ### Computing the left whiskering of the reflexive pointed homotopy ```agda module _ {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} (h : B →∗ C) (f : A →∗ B) where compute-refl-left-whisker-comp-pointed-htpy : pointed-2-htpy ( left-whisker-comp-pointed-htpy h f f (refl-pointed-htpy f)) ( refl-pointed-htpy (h ∘∗ f)) compute-refl-left-whisker-comp-pointed-htpy = refl-pointed-2-htpy (refl-pointed-htpy (h ∘∗ f)) ``` ### Computing the right whiskering of the reflexive pointed homotopy Consider two pointed maps `f := (f₀ , f₁) : A →∗ B` and `g := (g₀ , g₁) : B →∗ C`. We are constructing a pointed `2`-homotopy ```text right-whisker-comp-pointed-htpy (refl-pointed-htpy h) f ~∗ refl-pointed-htpy (g ∘∗ f) ``` The underlying homotopy of this pointed `2`-homotopy is `refl-htpy`. The base point coherence of this homotopy is an identification witnessing that the triangle ```text H₁ ap g₀ f₁ ∙ g₁ ------> refl ∙ (ap g₀ f₁ ∙ g₁) \ / refl \ / right-whisker-concat refl (ap g₀ f₁ ∙ g₁) ≐ refl \ / ∨ ∨ refl ∙ (ap g₀ f₁ ∙ g₁) ``` commutes. Here, the identification `H₁` is the vertical pasting of the upper square and the lower triangle in the diagram ```text refl g₀ (f₀ *) ------------> g₀ (f₀ *) \ / ap g₀ f₁ \ / ap g₀ f₁ ∨ refl ∨ g₀ * ----> g₀ * \ / g₁ \ / g₁ ∨ ∨ ∗. ``` The upper square in this diagram is the inverse naturality of the reflexive homotopy `refl-htpy` and the lower triangle in this diagram is the reflexive identification. Recall that the inverse naturality of the reflexive homotopy `inv-nat-htpy refl-htpy f₁` computes to the horizontally constant square of identifications. Furthermore, the vertical pasting of the horizontally constant square `right-unit` and any commuting triangle `refl` computes to `refl`. Therefore it follows that the identification `H₁` above is equal to `refl`, as was required to show. ```agda module _ {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} (h : B →∗ C) (f : A →∗ B) where htpy-compute-refl-right-whisker-comp-pointed-htpy : unpointed-htpy-pointed-htpy ( right-whisker-comp-pointed-htpy h h (refl-pointed-htpy h) f) ( refl-pointed-htpy (h ∘∗ f)) htpy-compute-refl-right-whisker-comp-pointed-htpy = refl-htpy coherence-point-compute-refl-right-whisker-comp-pointed-htpy : coherence-point-unpointed-htpy-pointed-htpy ( right-whisker-comp-pointed-htpy h h (refl-pointed-htpy h) f) ( refl-pointed-htpy (h ∘∗ f)) ( htpy-compute-refl-right-whisker-comp-pointed-htpy) coherence-point-compute-refl-right-whisker-comp-pointed-htpy = inv ( ( right-unit) ∙ ( ( ap ( λ t → vertical-pasting-coherence-square-coherence-triangle-identifications ( refl) ( ap (map-pointed-map h) (preserves-point-pointed-map f)) ( ap (map-pointed-map h) (preserves-point-pointed-map f)) ( refl) ( preserves-point-pointed-map h) ( preserves-point-pointed-map h) ( t) ( refl)) ( inv-nat-refl-htpy ( map-pointed-map h) ( preserves-point-pointed-map f))) ∙ ( right-whisker-concat-horizontal-refl-coherence-square-identifications ( ap (map-pointed-map h) (preserves-point-pointed-map f)) ( preserves-point-pointed-map h)))) compute-refl-right-whisker-comp-pointed-htpy : pointed-2-htpy ( right-whisker-comp-pointed-htpy h h (refl-pointed-htpy h) f) ( refl-pointed-htpy (h ∘∗ f)) pr1 compute-refl-right-whisker-comp-pointed-htpy = htpy-compute-refl-right-whisker-comp-pointed-htpy pr2 compute-refl-right-whisker-comp-pointed-htpy = coherence-point-compute-refl-right-whisker-comp-pointed-htpy ```