Definition invstruct_free_gr (X : hSet) : invstruct (@op (free_gr' X)) (pr2 (free_gr' X)). Proof. use make_invstruct. - use setquotfun. + exact fginv. + refine (iscomprelrelfun_generated_binopeqrel_rev (fginv_binopfun X) _). unfold iscomprelrelfun. apply free_gr_hrel_univ. * intros. apply pr2. * intro x. rewrite fginv_binopfun_homot. apply free_gr_hrel_in_rev. - apply make_isinv. + refine (setquotunivprop' _ _ _). * intro. apply isasetmonoid. * intro l. refine (maponpaths (λ x, x * _) (setquotunivcomm _ _ _ _ _) @ _). apply (iscompsetquotpr _ (fginv l * l) []). apply generated_free_gr_hrel_in_rev. + refine (setquotunivprop' _ _ _). * intro. apply isasetmonoid. * intro l. refine (maponpaths (λ x, _ * x) (setquotunivcomm _ _ _ _ _) @ _). apply (iscompsetquotpr _ (l * fginv l) []). apply generated_free_gr_hrel_in. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Combinatorics.Lists.