Definition abgrquot {X : abgr} (R : binopeqrel X) : abgr. Proof. exists (setwithbinopquot R). apply isabgrquot. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.