English
Relates whiskerRight and whiskerLeft with associators: whiskerRight (whiskerLeft F α) K = associator F α K ≪≫ whiskerLeft F (whiskerRight α K) ≪≫ associator^(-1).
Русский
Соотносит whiskerRight и whiskerLeft через ассоциаторы: whiskerRight (whiskerLeft F α) K = ассоциатор F α K ≪≫ whiskerLeft F (whiskerRight α K) ≪≫ ассоциатор^(-1).
LaTeX
$$$\\mathrm{whiskerRight}(\\mathrm{whiskerLeft}\\;F\\;α)\\;K = \\mathrm{Functor.associator}\\,\\_\\_\\_ \\; ≪≫ \\; \\mathrm{whiskerLeft}\\,F\\, (\\mathrm{whiskerRight}\\ α\\ K) \\; ≪≫ (\\mathrm{Functor.associator}\\,\\_\\_\\_).inv$$$
Lean4
theorem whiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) :
whiskerRight (whiskerLeft F α) K =
(Functor.associator _ _ _).hom ≫ whiskerLeft F (whiskerRight α K) ≫ (Functor.associator _ _ _).inv :=
by cat_disch
