English
The pentagon identity holds for the associator and coprod maps: a certain composition of coprod.map and associator morphisms equals another such composition, expressing coherence of coproduct associativity.
Русский
Пентaгональная связь когерентности копродукта: соответствующая композиция отображений копрода и ассоциатора приводит к эквивалентной композиции.
LaTeX
$$$ \\text{(coprod.map (coprod.associator W X Y).hom (id Z))} \\circ (\\text{coprod.associator } W (X \\sqcup Y) Z).hom \\circ (\\text{coprod.map } id_W (coprod.associator X Y Z).hom) = (\\text{coprod.associator } (W \\sqcup X) Y Z).hom \\circ (\\text{coprod.associator } W X (Y \\sqcup Z)).hom $$$
Lean4
theorem pentagon (W X Y Z : C) :
coprod.map (coprod.associator W X Y).hom (𝟙 Z) ≫
(coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) (coprod.associator X Y Z).hom =
(coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom :=
by simp
