Lemma abmonoid_iso_equiv (X Y : ob abmonoid_category) : z_iso X Y -> monoidiso (X : abmonoid) (Y : abmonoid). Proof. intro f. use make_monoidiso. - exact (make_weq (pr1 (pr1 f)) (abmonoid_iso_is_equiv X Y f)). - exact (pr2 (pr1 f)). 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.