Homotopy whiskering

Whiskering is the composition of homotopies with regular functions.

Definition

Given functions $fg:B\to C$ and a homotopy $H:f\sim g$, the whiskering operations are defined:

• For a function $h:A\to B$, we have a homotopy $h\cdot H:hf\sim hg$.

• For a function $h:C\to D$, we instead have a homotopy $H\cdot h:fh\sim gh$.[cite:@rijke2022introduction]