# Whiskering higher homotopies with respect to composition

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2024-02-06.

module foundation.whiskering-higher-homotopies-composition where

Imports
open import foundation.action-on-identifications-functions
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.homotopies


## Idea

Consider two dependent functions f g : (x : A) → B x equipped with two homotopies H H' : f ~ g, and consider a family of maps h : (x : A) → B x → C x. Then we obtain a map

  α ↦ ap h ·l α : H ~ H' → h ·l H ~ h ·l H'


This operation is called the left whiskering. Alternatively the left whiskering operation of 2-homotopies can be defined using the action on higher identifications of functions by

  α x ↦ ap² h (α x).


Similarly, the right whiskering is defined to be the operation

  (H ~ H') → (h : (x : A) → B x) → (H ·r h ~ H' ·r h)


given by

  α h ↦ α ·r h,


for any pair of homotopies H H' : f ~ g, where f g : (x : A) (y : B x) → C x y.

## Definitions

### Left whiskering higher homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
{f g : (x : A) → B x}
where

left-whisker-comp² :
(h : {x : A} → B x → C x) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H'
left-whisker-comp² h α = ap h ·l α


### Right whiskering higher homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
{f g : {x : A} (y : B x) → C x y} {H H' : {x : A} → f {x} ~ g {x}}
where

right-whisker-comp² :
(α : {x : A} → H {x} ~ H' {x}) (h : (x : A) → B x) → H ·r h ~ H' ·r h
right-whisker-comp² α h = α ·r h


### Double whiskering higher homotopies

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2}
{C : (x : A) → B x → UU l3} {D : (x : A) → B x → UU l4}
{f g : {x : A} (y : B x) → C x y} {H H' : {x : A} → f {x} ~ g {x}}
where

double-whisker-comp² :
(left : {x : A} {y : B x} → C x y → D x y)
(α : {x : A} → H {x} ~ H' {x})
(right : (x : A) → B x) →
left ·l H ·r right ~ left ·l H' ·r right
double-whisker-comp² left α right = double-whisker-comp (ap left) α right