Lemma iscomm_free_abmonoid (X : hSet) : iscomm (@op (free_abmonoid' X)). Proof. refine (setquotuniv2prop' _ _ _). - intros. apply (isasetmonoid (free_abmonoid' X)). - intros x1 x2. apply (iscompsetquotpr _ (x1 * x2) (x2 * x1)). apply generated_binopeqrel_intro, free_abmonoid_hrel_intro. 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.