Lemma isabgrdirprod (X Y : abgr) : isabgrop (@op (setwithbinopdirprod X Y)). Proof. exists (isgrdirprod X Y). apply (pr2 (isabmonoiddirprod X Y)). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.