Definition gr_equiv_weq_iso (X Y : ob gr_category) : (monoidiso (X : gr) (Y : gr)) ≃ (z_iso X Y). Proof. use make_weq. - exact (gr_equiv_iso X Y). - exact (gr_equiv_iso_is_equiv X Y). 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.