Proposition pb_preserves_bincoproduct_from_stable_bincoproducts (H : stable_bincoproducts BC) {x y : C} (f : x --> y) : preserves_bincoproduct (cod_pb PB f). Proof. use preserves_bincoproduct_if_preserves_chosen. { use bincoproducts_cod_fib. exact BC. } intros ag₁ bg₂. apply from_stable. exact H. 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.