# Whiskering pointed homotopies with respect to concatenation

Content created by Egbert Rijke.

Created on 2024-03-13.

module structured-types.whiskering-pointed-2-homotopies-concatenation where

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-triangles-of-identifications
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.universe-levels
open import foundation.whiskering-homotopies-concatenation
open import foundation.whiskering-identifications-concatenation

open import structured-types.pointed-2-homotopies
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types


## Idea

The whiskering operations of pointed 2-homotopies with respect to concatenation of pointed homotopies are two operations that produce pointed 2-homotopies between concatenations of pointed homotopies from either a pointed 2-homotopy on the left or on the right of the concatenations.

• The left whiskering is an operation that takes a pointed homotopy H : f ~∗ g and a pointed 2-homotopy α : K ~²∗ L between two pointed homotopies K L : g ~∗ h as indicated in the diagram

               K
H      ----->
f -----> g -----> h,
L


and returns a pointed 2-homotopy H ∙h K ~²∗ H ∙h L.

• The right whiskering is an operation that takes a pointed 2-homotopy α : H ~²∗ K between two pointed homotopies H K : f ~∗ g and a pointed homotopy L : g ~∗ h as indicated in the diagram

      H
----->
f -----> g -----> h,
K        L


and returns a pointed 2-homotopy H ∙h L ~²∗ K ∙h L.

## Definitions

### Left whiskering of pointed 2-homotopies with respect to concatenation

Consider three pointed maps f := (f₀ , f₁), g := (g₀ , g₁), and h := (h₀ , h₁) from A to B, a pointed homotopy H := (H₀ , H₁) : f ~∗ g and a pointed 2-homotopy α := (α₀ , α₁) : K ~²∗ L between two pointed homotopies K := (K₀ , K₁) and L := (L₀ , L₁) from g to h as indicated in the diagram

               K
H      ----->
f -----> g -----> h.
L


The underlying homotopy of the left whiskering H ·l∗ α : H ∙h K ~²∗ H ∙h L is the homotopy

  H₀ ·l α₀ : H₀ ∙h K₀ ~ H₀ ∙h L₀.


The base point coherence of this homotopy is an identification witnessing that the triangle

           (H ∙h K)₁
f₁ --------> ((H₀ *) ∙ (K₀ *)) ∙ h₁
\       /
(H ∙h L)₁ \     / right-whisker (left-whisker (H₀ *) (α₀ *)) h₁
\   /
∨ ∨
((H₀ *) ∙ (L₀ *)) ∙ h₁


commutes. Here, the identifications (H ∙h K)₁ and (H ∙h L)₁ are the horizontal pastings of the commuting triangles of identifications

       H₀ *      K₀ *                   H₀ *      L₀ *
f₀ * ---> g₀ * ----> h₀ *        f₀ * ---> g₀ * ----> h₀ *
\      |      /                  \      |      /
\  H₁ |  K₁ /                    \  H₁ |  L₁ /
f₁  \    |g₁  / h₁               f₁  \    |g₁  / h₁
\   |   /                        \   |   /
\  |  /                          \  |  /
∨ ∨ ∨                            ∨ ∨ ∨
*                                *.


Then the triangle

                   horizontal-pasting H₁ K₁
f₁ --------> (H₀ * ∙ K₀ *) ∙ h₁
\         /
\       /
horizontal-pasting H₁ L₁ \     / right-whisker (left-whisker (H₀ *) (α₀ *)) h₁
\   /
∨ ∨
(H₀ * ∙ K₀ *) ∙ h₁


commutes by left whiskering of horizontal pasting of commuting triangles of identifications.

module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{f g h : A →∗ B} (H : f ~∗ g) (K L : g ~∗ h) (α : K ~²∗ L)
where

htpy-left-whisker-concat-pointed-2-htpy :
unpointed-htpy-pointed-htpy
( concat-pointed-htpy H K)
( concat-pointed-htpy H L)
htpy-left-whisker-concat-pointed-2-htpy =
left-whisker-concat-htpy (htpy-pointed-htpy H) (htpy-pointed-2-htpy α)

coherence-point-left-whisker-concat-pointed-2-htpy :
coherence-point-unpointed-htpy-pointed-htpy
( concat-pointed-htpy H K)
( concat-pointed-htpy H L)
( htpy-left-whisker-concat-pointed-2-htpy)
coherence-point-left-whisker-concat-pointed-2-htpy =
left-whisker-horizontal-pasting-coherence-triangle-identifications
( preserves-point-pointed-map f)
( preserves-point-pointed-map g)
( preserves-point-pointed-map h)
( htpy-pointed-htpy H (point-Pointed-Type A))
( htpy-pointed-htpy K (point-Pointed-Type A))
( htpy-pointed-htpy L (point-Pointed-Type A))
( coherence-point-pointed-htpy H)
( coherence-point-pointed-htpy K)
( coherence-point-pointed-htpy L)
( htpy-pointed-2-htpy α (point-Pointed-Type A))
( coherence-point-pointed-2-htpy α)

left-whisker-concat-pointed-2-htpy :
concat-pointed-htpy H K ~²∗ concat-pointed-htpy H L
pr1 left-whisker-concat-pointed-2-htpy =
htpy-left-whisker-concat-pointed-2-htpy
pr2 left-whisker-concat-pointed-2-htpy =
coherence-point-left-whisker-concat-pointed-2-htpy


### Right whiskering of pointed 2-homotopies with respect to concatenation

Consider three pointed maps f := (f₀ , f₁), g := (g₀ , g₁), and h := (h₀ , h₁) from A to B, a pointed 2-homotopy α := (α₀ , α₁) : H ~²∗ K between two pointed homotopies H := (H₀ , H₁) and K := (K₀ , K₁) from f to g and a pointed homotopy L := (L₀ , L₁) : g ~∗ h as indicated in the diagram

      H
----->
f -----> g -----> h.
K        L


The underlying homotopy of the right whiskering α ·r∗ L : H ∙h L ~²∗ K ∙h L is the homotopy

  α₀ ·r L₀ : H₀ ∙h L₀ ~ K₀ ∙h L₀.


The base point coherence of this homotopy is an identification witnessing that the triangle

           (H ∙h L)₁
f₁ --------> ((H₀ *) ∙ (L₀ *)) ∙ h₁
\         /
(K ∙h L)₁ \       / right-whisker (right-whisker (α₀ *) (L₀ *)) h₁
\     /
∨   ∨
((K₀ *) ∙ (L₀ *)) ∙ h₁


commutes. Here, the identifications (H ∙h L)₁ and (K ∙h L)₁ are the horizontal pastings of the commuting triangles of identifications

       H₀ *      L₀ *                   K₀ *      L₀ *
f₀ * ---> g₀ * ----> h₀ *        f₀ * ---> g₀ * ----> h₀ *
\      |      /                  \      |      /
\  H₁ |  L₁ /                    \  K₁ |  L₁ /
f₁  \    |g₁  / h₁               f₁  \    |g₁  / h₁
\   |   /                        \   |   /
\  |  /                          \  |  /
∨ ∨ ∨                            ∨ ∨ ∨
*                                *.


Then the triangle

                   horizontal-pasting H₁ L₁
f₁ --------> (H₀ * ∙ L₀ *) ∙ h₁
\         /
\       /
horizontal-pasting K₁ L₁ \     / right-whisker (right-whisker (α₀ *) (L₀ *)) h₁
\   /
∨ ∨
(K₀ * ∙ L₀ *) ∙ h₁


commutes by right whiskering of horizontal pasting of commuting triangles of identifications.

module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
{f g h : A →∗ B} (H K : f ~∗ g) (α : H ~²∗ K) (L : g ~∗ h)
where

htpy-right-whisker-concat-pointed-2-htpy :
unpointed-htpy-pointed-htpy
( concat-pointed-htpy H L)
( concat-pointed-htpy K L)
htpy-right-whisker-concat-pointed-2-htpy =
right-whisker-concat-htpy (htpy-pointed-2-htpy α) (htpy-pointed-htpy L)

coherence-point-right-whisker-concat-pointed-2-htpy :
coherence-point-unpointed-htpy-pointed-htpy
( concat-pointed-htpy H L)
( concat-pointed-htpy K L)
( htpy-right-whisker-concat-pointed-2-htpy)
coherence-point-right-whisker-concat-pointed-2-htpy =
right-whisker-horizontal-pasting-coherence-triangle-identifications
( preserves-point-pointed-map f)
( preserves-point-pointed-map g)
( preserves-point-pointed-map h)
( htpy-pointed-htpy H (point-Pointed-Type A))
( htpy-pointed-htpy K (point-Pointed-Type A))
( htpy-pointed-htpy L (point-Pointed-Type A))
( coherence-point-pointed-htpy H)
( coherence-point-pointed-htpy K)
( coherence-point-pointed-htpy L)
( htpy-pointed-2-htpy α (point-Pointed-Type A))
( coherence-point-pointed-2-htpy α)

right-whisker-concat-pointed-2-htpy :
concat-pointed-htpy H L ~²∗ concat-pointed-htpy K L
pr1 right-whisker-concat-pointed-2-htpy =
htpy-right-whisker-concat-pointed-2-htpy
pr2 right-whisker-concat-pointed-2-htpy =
coherence-point-right-whisker-concat-pointed-2-htpy