proposition: 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: 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.
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