no goals
C : Type u₁
inst✝³ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq 0 0 biprod.inl biprod.inr
convert of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)