Proposition from_stable_in1 : dom_mor (cod_fiber_functor_pb PB f (BinCoproductIn1 (bincoproducts_cod_fib y BC ag₁ bg₂))) = BinCoproductIn1 apbp · from_stable_mor. Proof. unfold from_stable_mor ; cbn. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). - rewrite !assoc'. rewrite !PullbackArrow_PullbackPr1. unfold pb_bincoproduct_mor. rewrite BinCoproductIn1Commutes. apply idpath. - rewrite !assoc'. rewrite !PullbackArrow_PullbackPr2. unfold bincoproduct_pb_slice_mor. rewrite BinCoproductIn1Commutes. 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.