Definition abgrfunfromunit (X : abgr) : monoidfun unitabgr X := monoidfunconstr (abgrfunfromunit_ismonoidfun X).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.