Lemma gr_iso_equiv_is_equiv (X Y : gr_category) : isweq (gr_iso_equiv X Y). Proof. use isweq_iso. - exact (gr_equiv_iso X Y). - intros x. use z_iso_eq. use monoidfun_paths. use idpath. - intros y. use monoidiso_paths. use subtypePath. + intros x0. use isapropisweq. + use idpath. 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.