English
The isomorphism whiskerLeft composed twice satisfies a standard associativity coherence: isoWhiskerLeft F (isoWhiskerLeft G α) equals an appropriate composite formed with associators and isoWhiskerLeft of F⋙G and α.
Русский
Изоморфизм whiskerLeft дважды удовлетворяет стандартной когеренции ассоциативности: isoWhiskerLeft F (isoWhiskerLeft G α) равен композиции с ассоциаторами и isoWhiskerLeft(F⋙G) и α.
LaTeX
$$$\\mathrm{isoWhiskerLeft}\\,F\\,(\\mathrm{isoWhiskerLeft}\\,G\\;α) = (\\mathrm{Functor.associator}\\;\\_\\_\\_).symm \\; ≪≫ \\; \\mathrm{isoWhiskerLeft}\\,(F\\circ G)\\;α \\;≪≫ (\\mathrm{Functor.associator}\\;\\_\\_\\_)$$$
Lean4
@[simp]
theorem isoWhiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ≅ K) :
isoWhiskerLeft F (isoWhiskerLeft G α) =
(Functor.associator _ _ _).symm ≪≫ isoWhiskerLeft (F ⋙ G) α ≪≫ Functor.associator _ _ _ :=
by cat_disch
