Lemma ismonoidfuninvmap {X Y : monoid} (f : monoidiso X Y) : ismonoidfun (invmap (pr1 f)). Proof. exists (isbinopfuninvmap f). apply (invmaponpathsweq (pr1 f)). rewrite (homotweqinvweq (pr1 f)). apply (!pr2 (pr2 f)). Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.