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