Definition carrierofasubabgr {X : abgr} (A : subabgr X) : abgr. Proof. exists A. apply isabgrcarrier. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.