proposition: Lemma AdmMonoEnlargement {M:ExactCategory} {A B C:M} (BC : BinDirectSum B C) (i:A-->B) (f:A-->C) : isAdmissibleMonomorphism i -> isAdmissibleMonomorphism (ToBinDirectSum BC i f).
proof: Proof. intros I. apply (squash_to_hProp (to_hasBinDirectSums A C)); intros AC. assert (e : ToBinDirectSum BC i f = ι₁ · (1 + π₁·f·ι₂) · (directSumMap AC _ i 1)). { apply ToBinDirectSumsEq. - rewrite BinDirectSumPr1Commutes. rewrite assoc'. unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr1Commutes. rewrite assoc. rewrite rightDistribute. rewrite 2 leftDistribute. rewrite id_right. rewrite (to_IdIn1 AC). rewrite id_left. refine (! runax (A-->B) _ @ _). apply maponpaths. rewrite assoc. rewrite (assoc' _ _ π₁). rewrite (to_Unel2 AC). unfold to_unel. rewrite zeroRight, zeroLeft. reflexivity. - rewrite BinDirectSumPr2Commutes. rewrite assoc'. unfold directSumMap. unfold BinDirectSumIndAr. rewrite BinDirectSumPr2Commutes. rewrite assoc. rewrite rightDistribute. rewrite 2 leftDistribute. rewrite 2 id_right. rewrite (to_Unel1 AC). unfold to_unel. rewrite lunax. rewrite id_right. rewrite 2 assoc. rewrite (to_IdIn1 AC). rewrite id_left. rewrite assoc'. rewrite (to_IdIn2 AC). rewrite id_right. reflexivity. } induction (!e); clear e. apply EC_ComposeMono. - apply EC_ComposeMono. + apply In1IsAdmMono. + apply IsIsoIsMono. apply elem21_isiso. - now apply MonoPlusIdentity. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions