no goals
C : Type u
inst✝¹ : Category C
X✝ Y✝ : C
inst✝ : HasBinaryProducts 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