proposition: Lemma abgr_epi_cokernel_out_ismonoidfun {A B C : abgr} (f : abgr_category⟦A, B⟧) (isE : isEpi f) (h : abgr_category⟦A, C⟧) (H : KernelArrow (abgr_Kernel f) · h = ZeroArrow abgr_Zero _ _) : ismonoidfun (λ b : B, (pr1 (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H b)))).
proof: Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. set (HH0 := abgr_epi_cokernel_out_data_mult x x' f isE h H (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H x)) (iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H x'))). assert (HH : iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H (x * x')%multmonoid) = HH0). { set (tmp := abgr_epi_CokernelOut_iscontr f isE h H (x * x')%multmonoid). rewrite (pr2 tmp). use pathsinv0. rewrite (pr2 tmp). use idpath. } exact (base_paths _ _ HH). - assert (HH : iscontrpr1 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid) = abgr_epi_cokernel_out_data_unel f isE h H). { rewrite (pr2 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)). use pathsinv0. rewrite (pr2 (abgr_epi_CokernelOut_iscontr f isE h H 1%multmonoid)). use idpath. } exact (base_paths _ _ HH). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.Algebra.BinaryOperations UniMath.Algebra.Groups UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums