Lemma abmonoid_iso_is_equiv (A B : ob abmonoid_category) (f : z_iso A B) : isweq (pr1 (pr1 f)). Proof. use isweq_iso. - exact (pr1monoidfun _ _ (inv_from_z_iso f)). - intros x. use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x). intros x0. use isapropismonoidfun. - intros x. use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x). intros x0. use isapropismonoidfun. 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.