English
In a monoidal category with graded objects X1 and X3 and unit object, the associativity morphisms together with the unitors satisfy the usual triangle coherence: the two canonical ways of re-associating X1 ⊗ 1 ⊗ X3 down to X1 ⊗ X3 agree.
Русский
В моноидальной категории с градационными объектами X1 и X3 и единичным объектом выполняется обычная треугольная когерентность: два канонических способа перенастройки X1 ⊗ 1 ⊗ X3 к X1 ⊗ X3 совпадают.
LaTeX
$$$(\alpha_{X_1,\mathbf{1},X_3})^{\mathrm{hom}} \circ \mathrm{tensorHom}(\mathrm{id}_{X_1})\,(\mathrm{leftUnitor}_{X_3})^{\mathrm{hom}} = (\mathrm{rightUnitor}_{X_1})^{\mathrm{hom}}\,(\mathrm{id}_{X_3})^{\mathrm{hom}}$$$
Lean4
theorem triangle :
(associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom = tensorHom (rightUnitor X₁).hom (𝟙 X₃) :=
by
convert
mapBifunctor_triangle (curriedAssociatorNatIso C) (𝟙_ C) (rightUnitorNatIso C) (leftUnitorNatIso C)
(triangleIndexData I) X₁ X₃ (by simp)
all_goals assumption
