Definition reverse_binopfun (X : hSet) : binopfun (free_monoid X) (setwithbinop_rev (free_monoid X)). Proof. use make_binopfun. - exact reverse. - intros x x'. apply reverse_concatenate. 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.