Definition stable_from_pb_preserves_bincoproduct_mor_help : pb_sum --> ζ. Proof. use (BinCoproductArrow pb_sum (c := ζ)). - use make_cod_fib_mor. + exact (inv_from_z_iso φa · BinCoproductIn1 _). + abstract (cbn ; unfold bincoproduct_pb_slice_mor ; rewrite !assoc' ; rewrite BinCoproductIn1Commutes ; apply (PullbackArrow_PullbackPr2 (make_Pullback p H₁))). - use make_cod_fib_mor. + exact (inv_from_z_iso φb · BinCoproductIn2 _). + abstract (cbn ; unfold bincoproduct_pb_slice_mor ; rewrite !assoc' ; rewrite BinCoproductIn2Commutes ; apply (PullbackArrow_PullbackPr2 (make_Pullback q 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.