Lemma ismonoidop_concatenate (X : UU) : ismonoidop (@concatenate X). Proof. use make_ismonoidop. - use assoc_concatenate. - use make_isunital. + exact []. + use make_isunit. * use nil_concatenate. * use concatenate_nil. 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.