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