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. 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.
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.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence.