Lemma isMonic_to_binop_BinDirectSum2 {x y z : A} (f : x --> y) (g : Monic A 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_Pr2 DS = h · to_binop x DS (f · to_In1 DS) (g · to_In2 DS) · to_Pr2 DS). { rewrite 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_IdIn2 A _ _ _ _ _ _ _ DS) in e. rewrite (to_Unel1' DS) in e. rewrite ZeroArrow_comp_right in e. rewrite id_right in e. use (MonicisMonic A g). rewrite to_lunax'' 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.