English
The natural transformation mapWhiskerRight (F.associator G H).hom equals a composite built from mapCompLeft, whiskerRight, and mapPair.
Русский
Естественная трансформация mapWhiskerRight (F.associator G H).hom равна композиции из mapCompLeft, whiskerRight и mapPair.
LaTeX
$$$\operatorname{mapWhiskerRight}\_ (F \;\text{associator } G H)^{\mathrm{hom}} = (\operatorname{mapCompLeft} E (F \;\!\!\! \! G) H)^{\mathrm{hom}} \;\circ \; \mathrm{whiskerRight}(\operatorname{mapCompLeft} E F G)^{\mathrm{hom}} (\operatorname{mapPair} H (\mathbf{1}_E)) \circ ((\operatorname{mapPair} F (\mathbf{1}_E))^{\mathrm{associator}} (\operatorname{mapPair G (\mathbf{1}_E)} ) (\operatorname{mapPair H (\mathbf{1}_E)})).\mathrm{hom} \circ \mathrm{whiskerLeft}(\operatorname{mapPair F (\mathbf{1}_E)}) (\operatorname{mapCompLeft} E G H)^{\mathrm{inv}} \circ (\operatorname{mapCompLeft} E F (G \;\!\!\! \! H))^{\mathrm{inv}}$$$
Lean4
theorem mapWhiskerRight_leftUnitor_hom (F : A ⥤ B) :
mapWhiskerRight F.leftUnitor.hom (𝟭 C) =
(mapCompLeft C (𝟭 A) F).hom ≫ whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom :=
by apply natTrans_ext <;> ext <;> simp [mapCompLeft]
