# Whiskering of pointed homotopies with respect to composition of pointed maps

Content created by Egbert Rijke.

Created on 2024-03-13.

module structured-types.whiskering-pointed-homotopies-composition where

Imports
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


## Idea

The whiskering operations of pointed homotopies with respect to composition of pointed maps 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

      f
----->     h
A -----> B -----> C.
g


The left whiskering operation on pointed homotopies of h and H is a pointed homotopy

  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

               g
f      ----->
A -----> B -----> C.
h


The right whiskering operation on pointed homotopies of H and f is a pointed homotopy

  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

  h ·l∗ H : (h ∘∗ f) ~∗ (h ∘∗ g).


Construction. The underlying homotopy of h ·l∗ H is the whiskered homotpy

  h₀ ·l H₀.


For the coherence, we have to show that the triangle

            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 with respect to concatenation it suffices to show that the triangle

           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

        H₀ *
f₀ * ------> g₀ *
\       /
f₁ \     / g₁
\   /
∨ ∨
*


commutes.

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

  H ·r∗ f : (g ∘∗ f) ~∗ (h ∘∗ f).


Construction. The underlying homotopy of H ·r∗ f is the homotopy

  H₀ ·r f₀ : (g₀ ∘ f₀) ~ (h₀ ∘ f₀).


Then we have to show that the outer triangle in the diagram

              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₁).

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

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

  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

                   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

                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.

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