English
For a StrongTrans θ: G ⇝ H between oplax functors and morphisms f,g,h as in the statement, the left-hand side equals the right-hand side expressing the interaction of mapComp with naturality and associators under right whiskering.
Русский
Для StrongTrans θ: G ⇝ H между оплазными функторными системами и морфизмами f,g,h как в утверждении, левая и правая части равны, выражая взаимодействие mapComp с натуральностью и ассоциаторами под правым взвешиванием.
LaTeX
$$$(\eta.naturality (f \gg g)).hom \; ⊗ \; h \; ⟶ \; (\alpha_{_\, _\, _}).hom \; ⟶ \; F.map f ◁ (\eta.naturality g).hom$$
Lean4
@[reassoc (attr := simp), to_app]
theorem whiskerRight_naturality_comp (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :
(η.naturality (f ≫ g)).hom ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
F.mapComp f g ▷ η.app c ▷ h ≫
(α_ _ _ _).hom ▷ h ≫
(α_ _ _ _).hom ≫
F.map f ◁ (η.naturality g).hom ▷ h ≫
(α_ _ _ _).inv ≫
(α_ _ _ _).inv ▷ h ≫ (η.naturality f).hom ▷ G.map g ▷ h ≫ (α_ _ _ _).hom ▷ h ≫ (α_ _ _ _).hom :=
η.toOplax.whiskerRight_naturality_comp _ _ _
