Proposition from_stable : isBinCoproduct (C/x) (cod_pb PB f ag₁) (cod_pb PB f bg₂) (cod_pb PB f (bincoproducts_cod_fib y BC ag₁ bg₂)) (#(cod_pb PB f) (BinCoproductIn1 (bincoproducts_cod_fib y BC ag₁ bg₂))) (#(cod_pb PB f) (BinCoproductIn2 (bincoproducts_cod_fib y BC ag₁ bg₂))). Proof. use to_bincoproduct_slice. rewrite !cod_fiber_functor_on_mor. use (isBinCoproduct_z_iso (isBinCoproduct_BinCoproduct _ apbp)). - use make_z_iso. + exact from_stable_mor. + exact from_stable_inv. + exact from_stable_inverses. - exact from_stable_in1. - exact from_stable_in2. 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.