no goals
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : Category C
inst✝ : HasBinaryCoproducts C
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨿ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨿ X) Y Z).hom ≫ (associator W X (Y ⨿ Z)).hom
simp