Lemma mor_from_mono_cod_bincoproduct_mor_eq : bincoproduct_ob_epi · bincoproduct_ob_mor_mono_cod = ζ · mono_cod_mor gz. Proof. unfold ζ, mor_from_mono_cod_bincoproduct_from_sum. use BinCoproductArrowsEq. - rewrite bincoproduct_ob_comm. rewrite !assoc. unfold sum_mor_mono_cod. rewrite !BinCoproductIn1Commutes. refine (_ @ !(mono_mor_eq φp)). apply idpath. - rewrite bincoproduct_ob_comm. rewrite !assoc. unfold sum_mor_mono_cod. rewrite !BinCoproductIn2Commutes. refine (_ @ !(mono_mor_eq ψ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.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.DisjointBinCoproducts. Require Import UniMath.CategoryTheory.Limits.StrictInitial. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.Inclusion. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpiFacts.