Definition stable_bincoproducts : UU := ∏ (a b x y ap bp : C) (f : x --> y) (g₁ : a --> y) (g₂ : b --> y) (π₁ : ap --> a) (π₂ : ap --> x) (ρ₁ : bp --> b) (ρ₂ : bp --> x) (p : π₁ · g₁ = π₂ · f) (q : ρ₁ · g₂ = ρ₂ · f) (H₁ : isPullback p) (H₂ : isPullback q), isPullback (bincoproduct_pb_diag p q).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Section FromStable. End FromStable.