Lemma gr_equiv_is_iso (X Y : ob gr_category) (f : monoidiso (X : gr) (Y : gr)) : @is_z_isomorphism gr_precategory 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.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.