Lemma sumofmaps_free_gr_unit {X : hSet} : sumofmaps free_gr_unit (grinv (free_gr X) ∘ free_gr_unit) ~ @presented_monoid_intro (setcoprod X X) (free_gr_hrel X). Proof. intro x. induction x as [x|x]; reflexivity. 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.