Definition invertible_submonoid_grop X : isgrop (@op (invertible_submonoid X)). Proof. pose (submon := invertible_submonoid X). pose (submon_carrier := ismonoidcarrier submon). apply (isgropif submon_carrier). intros xpair. pose (x := pr1 xpair). pose (unel := unel_is submon_carrier). apply (squash_to_prop (pr2 xpair) (propproperty _)). intros xinv. unfold haslinv. apply hinhpr. refine ((pr1 xinv,, inverse_in_submonoid _ x (pr1 xinv) (pr2 xpair) (pr2 xinv)),, _). apply subtypePath_prop. exact (pr2 (pr2 xinv)). Defined.
Require Import UniMath.MoreFoundations.Subtypes.