Proposition to_bincoproduct_slice_mor_eq : to_bincoproduct_slice_mor_mor · cod_mor h = cod_mor s. Proof. unfold to_bincoproduct_slice_mor_mor. use (BinCoproductArrowsEq _ _ _ coprod). - rewrite !assoc. rewrite (BinCoproductIn1Commutes _ _ _ coprod) ; cbn. rewrite (mor_eq ρ₁), (mor_eq ι₁). apply idpath. - rewrite !assoc. rewrite (BinCoproductIn2Commutes _ _ _ coprod) ; cbn. rewrite (mor_eq ρ₂), (mor_eq ι₂). apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.