unit_naturality — Mathlib

English

For a monad T, and any morphism f: X → Y, the unit η satisfies f ≫ η_Y = η_X ≫ T.map f.

Русский

Для монадой T и для любого отображения f: X → Y выполняется nатрaльность единицы: f ∘ η_Y = η_X ∘ T.map f.

LaTeX

$$$f \\;\\\\circ \\\\eta_Y = \\\\eta_X \\\\circ T.map f.$$$

Lean4

@[reassoc]
theorem unit_naturality (T : Monad C) ⦃X Y : C⦄ (f : X ⟶ Y) : f ≫ T.η.app Y = T.η.app X ≫ T.map f :=
  T.η.naturality _

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