proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums