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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. 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. @ZeroArrowFrom abgr_category abgr_Zero A = abgrfunfromunit A.