English
In a category with binary coproducts and terminal object, the associator and left/right unitor satisfy a triangle-like relation: (associator X ⊤ Y).hom ≫ map(id_X) (leftUnitor Y).hom = map(rightUnitor X) (id_Y).
Русский
В категории с бинарными копродуктами и терминальным объектом соблюдается треугольное отношение между ассоциатором и юниторами: (associator X ⊥ Y).hom ≫ map(id_X) (leftUnitor Y).hom = map(rightUnitor X) (id_Y).
LaTeX
$$$ (\\operatorname{coprod.associator} X (\\top) Y).hom \\circ \\operatorname{coprod.map}(\\mathrm{id}_X, \\operatorname{coprod.leftUnitor} Y).hom = \\operatorname{coprod.map}(\\operatorname{coprod.rightUnitor} X).hom (\\mathrm{id}_Y) $$$
Lean4
theorem triangle [HasBinaryProducts C] (X Y : C) :
(prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) (prod.leftUnitor Y).hom =
prod.map (prod.rightUnitor X).hom (𝟙 Y) :=
by ext <;> simp
