whiskerLeft_naturality_naturality

English

Natural transformation for left whiskering in StrongTrans for Pseudofunctors.

Русский

Натуральность левого взвешивания для преобразований между псевдофункторными связками в StrongTrans.

LaTeX

$$$f \triangleleft (\theta.naturality (g \gg h)).hom \; ≫ \dots$$$

Lean4

@[reassoc (attr := simp), to_app]
theorem whiskerLeft_naturality_naturality (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) :
    f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ (θ.naturality h).hom = f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β :=
  θ.toOplax.whiskerLeft_naturality_naturality _ _

Похожие утверждения