Definition gr_precategory_data : precategory_data := make_precategory_data gr_precategory_ob_mor (λ (X : gr), ((idmonoidiso X) : monoidfun X X)) (fun (X Y Z : gr) (f : monoidfun X Y) (g : monoidfun Y Z) => monoidfuncomp f g). Local Lemma gr_id_left (X Y : gr) (f : monoidfun X Y) : monoidfuncomp (idmonoidiso X) f = f. Proof. 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.