no goals
C : Type u
inst✝³ : Category C
X✝ Y✝ X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryCoproduct Z W
inst✝¹ : HasBinaryCoproduct Y W
inst✝ : HasBinaryCoproduct X W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)
simp