English
The double whiskeringRight satisfies a coherence relation with associators: whiskerRight (whiskerRight α F) G equals the associator-isomorphism composition with α and G; i.e., whiskerRight (whiskerRight α F) G = associator F G ≪≫ whiskerRight α (F ⋙ G) ≪≫ associator^(-1).
Русский
Двойное отбрасывание справа удовлетворяет когеренциям: whiskerRight (whiskerRight α F) G = ассоциатковое изоморфизмное композиция с α и G.
LaTeX
$$$\\mathrm{whiskerRight}(\\mathrm{whiskerRight}\\,α\\,F)\\,G = \\mathrm{Functor.associator}\\,\\_\\_\\_ \\; ≪≫ \\; \\mathrm{whiskerRight}\\,α\\,(F\\circ G) \\; ≪≫ (\\mathrm{Functor.associator}\\,\\_\\_\\_).inv$$$
Lean4
@[simp]
theorem whiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) :
whiskerRight (whiskerRight α F) G =
(Functor.associator _ _ _).hom ≫ whiskerRight α (F ⋙ G) ≫ (Functor.associator _ _ _).inv :=
by cat_disch
