Lemma isMonic_to_binop_BinDirectSum1 {x y z : A} (f : Monic A x y) (g : x --> z) (DS : BinDirectSum y z) : isMonic (to_binop _ _ (f · to_In1 DS) (g · to_In2 DS)). Proof. use make_isMonic. intros x0 g0 h X. assert (e : g0 · to_binop x DS (f · to_In1 DS) (g · to_In2 DS) · to_Pr1 DS = h · to_binop x DS (f · to_In1 DS) (g · to_In2 DS) · to_Pr1 DS). { etrans. apply maponpaths_2. apply X. apply idpath. } rewrite <- assoc in e. rewrite <- assoc in e. rewrite (@to_postmor_linear' A) in e. rewrite <- assoc in e. rewrite <- assoc in e. rewrite (to_IdIn1 DS) in e. rewrite (to_Unel2' DS) in e. rewrite ZeroArrow_comp_right in e. rewrite id_right in e. use (MonicisMonic A f). rewrite to_runax'' in e. exact e. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.