Definition pb_preserves_bincoproduct_weq_stable : stable_bincoproducts BC ≃ (∏ (x y : C) (f : x --> y), preserves_bincoproduct (cod_pb PB f)). Proof. use weqimplimpl. - exact @pb_preserves_bincoproduct_from_stable_bincoproducts. - exact stable_bincoproducts_from_pb_preserves_bincoproduct. - abstract (apply isaprop_stable_bincoproducts). - abstract (do 3 (use impred ; intro) ; apply isaprop_preserves_bincoproduct). 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.