Proposition bincoproduct_pb_diag {a b x y ap bp : C} {f : x --> y} {g₁ : a --> y} {g₂ : b --> y} {π₁ : ap --> a} {π₂ : ap --> x} {ρ₁ : bp --> b} {ρ₂ : bp --> x} (p : π₁ · g₁ = π₂ · f) (q : ρ₁ · g₂ = ρ₂ · f) : pb_bincoproduct_mor π₁ ρ₁ · bincoproduct_slice_mor g₁ g₂ = bincoproduct_pb_slice_mor π₂ ρ₂ · f. Proof. unfold bincoproduct_slice_mor, bincoproduct_pb_slice_mor, pb_bincoproduct_mor. use BinCoproductArrowsEq ; cbn. - rewrite !assoc. rewrite !BinCoproductIn1Commutes. rewrite !assoc'. rewrite BinCoproductIn1Commutes. rewrite p. apply idpath. - rewrite !assoc. rewrite !BinCoproductIn2Commutes. rewrite !assoc'. rewrite BinCoproductIn2Commutes. rewrite q. 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.