Definition monoidfuntounit (X : monoid) : monoidfun X unitmonoid := monoidfunconstr (monoidfuntounit_ismonoidfun X).
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.