Lemma isapropissubgr {X : gr} (A : hsubtype X) : isaprop (issubgr A). Proof. apply (isofhleveldirprod 1). - apply isapropissubmonoid. - apply impred. intro x. apply impred. intro a. apply (pr2 (A (x^-1))). Defined.
Require Import UniMath.MoreFoundations.Subtypes.