Proposition stable_from_pb_preserves_bincoproduct_inv_eq : stable_from_pb_preserves_bincoproduct_inv · cod_mor pb_sum = cod_mor ζ. Proof. cbn. unfold stable_from_pb_preserves_bincoproduct_inv. unfold bincoproduct_pb_slice_mor. use BinCoproductArrowsEq. - rewrite !assoc. rewrite !BinCoproductIn1Commutes. rewrite !assoc'. assert (dom_mor (BinCoproductIn1 pb_sum) = dom_mor (#(cod_pb PB f) ι₁)) as r. { apply idpath. } rewrite r. rewrite cod_fiber_functor_on_mor. cbn. rewrite PullbackArrow_PullbackPr2. unfold from_Pullback_to_Pullback. rewrite PullbackArrow_PullbackPr2. apply idpath. - rewrite !assoc. rewrite !BinCoproductIn2Commutes. rewrite !assoc'. assert (dom_mor (BinCoproductIn2 pb_sum) = dom_mor (#(cod_pb PB f) ι₂)) as r. { apply idpath. } rewrite r. rewrite cod_fiber_functor_on_mor. cbn. rewrite PullbackArrow_PullbackPr2. unfold from_Pullback_to_Pullback. rewrite PullbackArrow_PullbackPr2. apply idpath. Qed.
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.