proposition: Lemma iscomm_free_abgr (X : hSet) : iscomm (@op (free_abgr' X)).
proof: Proof. refine (setquotuniv2prop' _ _ _). - intros. apply (isasetmonoid (free_abgr' X)). - intros x1 x2. apply (iscompsetquotpr _ (x1 * x2) (x2 * x1)). apply generated_binopeqrel_intro, free_abgr_hrel_intro. Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists