Definition isgrcarrier {X : gr} (A : subgr X) : isgrop (@op A) := ismonoidcarrier A ,, (λ a : A, make_carrier _ ((pr1 a)^-1) (pr2 (pr2 A) (pr1 a) (pr2 a))) ,, isinvoncarrier A.
Require Import UniMath.MoreFoundations.Subtypes.