Proposition stable_from_pb_preserves_bincoproduct : isPullback (bincoproduct_pb_diag BC p q). Proof. simple refine (isPullback_z_iso _ _ (isPullback_Pullback pb) _ _ _). - exact stable_from_pb_preserves_bincoproduct_z_iso. - exact stable_from_pb_preserves_bincoproduct_left. - exact stable_from_pb_preserves_bincoproduct_right. Defined.
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.