Lemma isabgrcarrier {X : abgr} (A : subgr X) : isabgrop (@op A). Proof. exists (isgrcarrier A). apply (pr2 (@isabmonoidcarrier X A)). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.