# Whiskering operations

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-02-06.

module foundation.whiskering-operations where

Imports
open import foundation.universe-levels


## Idea

Consider a type A with a binary relation R : A → A → 𝒰, which comes equipped with a multiplicative operation

  μ : (x y z : A) → R x y → R y z → R x z.


Furthermore, assume that each R x y comes equipped with a further binary relation E : R x y → R x y → 𝒰. A left whiskering operation on E with respect to μ is an operation

  (f : R x y) {g h : R y z} → E g h → E (μ f g) (μ f h).


Similarly, a right whiskering operation on E with respect to μ is an operation

  {g h : R x y} → E g h → (f : R y z) → E (μ g f) (μ h f).


The general notion of whiskering is introduced in order to establish a clear naming scheme for all the variations of whiskering that exist in the agda-unimath library:

1. In whiskering identifications with respect to concatenation we define the whiskering operations

  left-whisker-concat :
(p : x ＝ y) {q r : y ＝ z} → q ＝ r → p ∙ q ＝ p ∙ r


and

  right-whisker-concat :
{p q : x ＝ y} → p ＝ q → (r : y ＝ z) → p ∙ r ＝ q ∙ r


with respect to concatenation of identifications.

2. In whiskering homotopies with respect to composition we define the whiskering operations

  left-whisker-comp :
(f : B → C) {g h : A → B} → g ~ h → f ∘ g ~ f ∘ h


and

  right-whisker-comp :
{f g : B → C} → (f ~ g) → (h : A → B) → f ∘ h ~ g ∘ h


of homotopies with respect to composition of functions.

3. In whiskering homotopies with respect to concatenation we define the whiskering operations

  left-whisker-comp-concat :
(H : f ~ g) {K L : g ~ h} → K ~ L → H ∙h K ~ H ∙h L


and

  right-whisker-comp-concat :
{H K : f ~ g} → H ~ K → (L : g ~ h) → H ∙h L ~ K ∙h L


of homotopies with respect to concatenation of homotopies.

4. In whsikering higher homotopies with respect to composition we define the whiskering operations

  left-whisker-comp² :
(f : B → C) {g h : A → B} {H K : g ~ h} → H ~ K → f ·l H ~ f ·l K


and

  right-whisker-comp² :
{f g : B → C} {H K : f ~ g} → H ~ K → (h : A → B) → H ·r h ~ K ·r h


of higher homotopies with respect to composition of functions.

## Definitions

### Left whiskering operations

module _
{l1 l2 l3 : Level} (A : UU l1) (R : A → A → UU l2)
where

left-whiskering-operation :
(μ : {x y z : A} → R x y → R y z → R x z) →
({x y : A} → R x y → R x y → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
left-whiskering-operation μ E =
{x y z : A} (f : R x y) {g h : R y z} → E g h → E (μ f g) (μ f h)

left-whiskering-operation' :
(μ : {x y z : A} → R y z → R x y → R x z) →
({x y : A} → R x y → R x y → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
left-whiskering-operation' μ E =
{x y z : A} (f : R y z) {g h : R x y} → E g h → E (μ f g) (μ f h)


### Right whiskering operations

module _
{l1 l2 l3 : Level} (A : UU l1) (R : A → A → UU l2)
where

right-whiskering-operation :
(μ : {x y z : A} → R x y → R y z → R x z) →
({x y : A} → R x y → R x y → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
right-whiskering-operation μ E =
{x y z : A} {f g : R x y} → E f g → (h : R y z) → E (μ f h) (μ g h)

right-whiskering-operation' :
(μ : {x y z : A} → R y z → R x y → R x z) →
({x y : A} → R x y → R x y → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
right-whiskering-operation' μ E =
{x y z : A} {f g : R y z} → E f g → (h : R x y) → E (μ f h) (μ g h)


### Double whiskering operations

Double whiskering operations are operations that simultaneously perform whiskering on the left and on the right.

Note that double whiskering should not be confused with iterated whiskering on the left or with iterated whiskering on the right.

module _
{l1 l2 l3 : Level} (A : UU l1) (R : A → A → UU l2)
where

double-whiskering-operation :
(μ : {x y z : A} → R x y → R y z → R x z) →
({x y : A} → R x y → R x y → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
double-whiskering-operation μ E =
{x' x y y' : A} (h : R x' x) {f g : R x y} (e : E f g) (k : R y y') →
E (μ (μ h f) k) (μ (μ h g) k)

double-whiskering-operation' :
(μ : {x y z : A} → R y z → R x y → R x z) →
({x y : A} → R x y → R x y → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
double-whiskering-operation' μ E =
{x' x y y' : A} (h : R y y') {f g : R x y} (e : E f g) (k : R x' x) →
E (μ (μ h f) k) (μ (μ h g) k)