English
The double whiskeringLeft satisfies a coherence relation with associators: whiskerLeft F (whiskerLeft G α) equals the left-hand side built from associators and whiskerLeft of F⋙G with α, up to associativity isomorphisms.
Русский
Двойное отбрасывание слева удовлетворяет когерентному отношению с ассоциаторами: whiskerLeft F (whiskerLeft G α) равно выражению через ассоциаторы и whiskerLeft F⋙G применяя α.
LaTeX
$$$\\mathrm{whiskerLeft}\\,F\\, (\\mathrm{whiskerLeft}\\,G\\,α) = (\\mathrm{Functor.associator}\\,\\__\\_\\_\\_).\\mathrm{inv} \\; \\circ \\mathrm{whiskerLeft}(F\\,\\circ G)\\; α \\circ (\\mathrm{Functor.associator}\\,\\__\\_\\_\\_).hom$$$
Lean4
@[simp]
theorem whiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) :
whiskerLeft F (whiskerLeft G α) =
(Functor.associator _ _ _).inv ≫ whiskerLeft (F ⋙ G) α ≫ (Functor.associator _ _ _).hom :=
by cat_disch
