# Whiskering operations

```agda
module foundation.whiskering-operations where
```

<details><summary>Imports</summary>

```agda
open import foundation.universe-levels
```

</details>

## Idea

Consider a type `A` with a [binary relation](foundation.binary-relations.md)
`R : A โ†’ A โ†’ ๐’ฐ`, which comes equipped with a multiplicative operation

```text
  ฮผ : (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
{{#concept "left whiskering operation" Agda=left-whiskering-operation}} on `E`
with respect to `ฮผ` is an operation

```text
  (f : R x y) {g h : R y z} โ†’ E g h โ†’ E (ฮผ f g) (ฮผ f h).
```

Similarly, a
{{#concept "right whiskering operation" Agda=right-whiskering-operation}} on `E`
with respect to `ฮผ` is an operation

```text
  {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](foundation.whiskering-identifications-concatenation.md)
   we define the whiskering operations

   ```text
     left-whisker-concat :
       (p : x ๏ผ y) {q r : y ๏ผ z} โ†’ q ๏ผ r โ†’ p โˆ™ q ๏ผ p โˆ™ r
   ```

   and

   ```text
     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](foundation.whiskering-homotopies-composition.md)
   we define the whiskering operations

   ```text
     left-whisker-comp :
       (f : B โ†’ C) {g h : A โ†’ B} โ†’ g ~ h โ†’ f โˆ˜ g ~ f โˆ˜ h
   ```

   and

   ```text
     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](foundation.whiskering-homotopies-concatenation.md)
   we define the whiskering operations

   ```text
     left-whisker-comp-concat :
       (H : f ~ g) {K L : g ~ h} โ†’ K ~ L โ†’ H โˆ™h K ~ H โˆ™h L
   ```

   and

   ```text
     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](foundation.whiskering-higher-homotopies-composition.md)
   we define the whiskering operations

   ```text
     left-whisker-compยฒ :
       (f : B โ†’ C) {g h : A โ†’ B} {H K : g ~ h} โ†’ H ~ K โ†’ f ยทl H ~ f ยทl K
   ```

   and

   ```text
     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

```agda
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

```agda
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.

```agda
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)
```