Definition abgrdirprod (X Y : abgr) : abgr. Proof. exists (setwithbinopdirprod X Y). apply isabgrdirprod. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.