triangle — Mathlib

English

The triangle axiom relates the associator and the unitors, ensuring coherence of the monoidal structure.

Русский

Треугольное тождение связывает ассоциатор и униторы, обеспечивая когерентность моноидальной структуры.

LaTeX

$$$\text{triangle identity: } a \otimes I \cong a \cong I \otimes a$$$

Lean4

theorem triangle (X Y : Dial C) :
    (associator X (𝟙_ (Dial C)) Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = tensorHom (rightUnitor X).hom (𝟙 Y) := by
  cat_disch

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