proposition: Lemma abmonoid_equiv_is_z_iso (X Y : ob abmonoid_category) (f : monoidiso (X : abmonoid) (Y : abmonoid)) : @is_z_isomorphism abmonoid_category X Y (monoidfunconstr (pr2 f)).
proof: Proof. exists (monoidfunconstr (pr2 (invmonoidiso f))). use make_is_inverse_in_precat. - use monoidfun_paths. use funextfun. intros x. use homotinvweqweq. - use monoidfun_paths. use funextfun. intros y. use homotweqinvweq. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence