Lemma nat_nat_prod_abgr_monoidfun_paths {A B : abgr} (a1 a2 : A) (f : monoidfun A B) (H : f a1 = f a2) : monoidfuncomp (nat_nat_prod_abmonoid_monoidfun a1) f = monoidfuncomp (nat_nat_prod_abmonoid_monoidfun a2) f. Proof. use monoidfun_paths. use funextfun. intros x. induction x as [x1 x2]. cbn. unfold nataddabmonoid_nataddabmonoid_to_monoid_fun. unfold nat_nat_to_monoid_fun. Opaque nat_to_monoid_fun. cbn. use (pathscomp0 (binopfunisbinopfun f _ _)). use (pathscomp0 _ (! (binopfunisbinopfun f _ _))). cbn. rewrite (monoidfun_nat_to_monoid_fun f a1 x1). rewrite (monoidfun_nat_to_monoid_fun f a2 x1). rewrite (monoidfun_nat_to_monoid_fun f (grinv A a1) x2). rewrite (monoidfun_nat_to_monoid_fun f (grinv A a2) x2). use two_arg_paths. - induction H. use idpath. - assert (e : f (grinv A a1) = f (grinv A a2)). { use (@grlcan B _ _ (pr1 f a1)). use (pathscomp0 (! binopfunisbinopfun f a1 (grinv A a1))). use (pathscomp0 (maponpaths (pr1 f) (grrinvax A a1))). cbn in H. rewrite H. use (pathscomp0 _ (binopfunisbinopfun f a2 (grinv A a2))). use (pathscomp0 _ (! (maponpaths (pr1 f) (grrinvax A a2)))). use idpath. } induction e. use idpath. 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.