Definition abgrshomabgr (X Y : abgr) : abgr. Proof. use make_abgr. - exact (abmonoidshomabmonoid X Y). - exact (abgrshomabgr_isabgrop X Y). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.