Definition idmonoidiso (X : monoid) : monoidiso X X. Proof. use make_monoidiso. - exact (idweq X). - use make_dirprod. + intros x x'. use idpath. + use idpath. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.