no goals
C : Type u₁
inst✝³ : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ IsPushout 0 0 coprod.inl coprod.inr
convert @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial