whiskerRight_naturality_id — Mathlib

English

Expresses a canonical isomorphism describing naturality at the identity morphism for a StrongTrans between pseudofunctors.

Русский

Каноническое изоморфизмное выражение натуральности на тождественный морфизм между псевдофункторными связками.

LaTeX

$$$\alpha \;\mathrm{naturality} (\mathrm{Id} a)$$$

Lean4

@[reassoc (attr := simp), to_app]
theorem whiskerRight_naturality_id (f : G.obj a ⟶ a') :
    (η.naturality (𝟙 a)).hom ▷ f ≫ (α_ _ _ _).hom ≫ η.app a ◁ (G.mapId a).hom ▷ f =
      (F.mapId a).hom ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ _ _ _).hom :=
  η.toOplax.whiskerRight_naturality_id _

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