English
There is a natural interchange between whiskering on the left and on the right: whiskerLeft then whiskerRight equals whiskerRight then whiskerLeft with appropriate arguments.
Русский
Существует естественный обмен между левым и правым whisker: whiskerLeft затем whiskerRight равны whiskerRight затем whiskerLeft с соответствующими аргументами.
LaTeX
$$$\\mathrm{whisker\\,exchange}(F,G;I,J)\\;:\\; \\mathrm{whiskerLeft}\\,F\\,β \\;\\circ\\; \\mathrm{whiskerRight}\\,α\\,I = \\mathrm{whiskerRight}\\,α\\,H \\circ \\mathrm{whiskerLeft}\\,G\\,β$$$
Lean4
theorem whisker_exchange {F G : EnrichedFunctor V C D} {H I : EnrichedFunctor V D E} (α : F ⟶ G) (β : H ⟶ I) :
whiskerLeft F β ≫ whiskerRight α I = whiskerRight α H ≫ whiskerLeft G β :=
by
ext X
simp only [EnrichedFunctor.forget_obj, EnrichedFunctor.comp_obj, EnrichedFunctor.category_comp_out, NatTrans.comp_app,
whiskerLeft_out_app, whiskerRight_out_app]
exact (β.out.naturality (α.out.app (ForgetEnrichment.of V X))).symm
