proposition: Lemma abgr_monoidfun_precomp {A :abmonoid} {B C : abgr} (f1 f2 : monoidfun B C) (g : monoidfun A B) (H : issurjective (pr1 g)) : monoidfuncomp g f1 = monoidfuncomp g f2 -> f1 = f2.
proof: Proof. intros e. use monoidfun_paths. use funextfun. intros x. use (squash_to_prop (H x) (setproperty C _ _)). intros hf. rewrite <- (hfiberpr2 _ _ hf). exact (toforallpaths _ _ _ (base_paths _ _ e) (hfiberpr1 _ _ hf)). 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