English
Pentagon coherence for functor composition and whiskering: isoWhiskerRight (associator F G H) K ≪≫ associator F (G ⋙ H) K ≪≫ isoWhiskerLeft F (associator G H K) = associator (F ⋙ G) H K ≪≫ associator F G (H ⋙ K).
Русский
Пентакональная когерентность для композиции функторов и отбрасываний: …
LaTeX
$$$\\mathrm{isoWhiskerRight}(\\mathrm{associator}\\;F\\;G\\;H)\\;K \\;≪≫ \\; \\mathrm{associator}\\;F\\;(G\\;⋙\\;H)\\;K \\;≪≫ \\; \\mathrm{isoWhiskerLeft}\\,F\\;(\\mathrm{associator}\\;G\\;H\\;K) = \\mathrm{associator}\\;(F\\;⋙\\;G)\\;H\\;K \\;≪≫ \\; \\mathrm{associator}\\;F\\;G\\;(H\\;⋙\\;K).$$$
Lean4
@[reassoc]
theorem pentagonIso :
isoWhiskerRight (associator F G H) K ≪≫ associator F (G ⋙ H) K ≪≫ isoWhiskerLeft F (associator G H K) =
associator (F ⋙ G) H K ≪≫ associator F G (H ⋙ K) :=
by cat_disch
