Definition gr_merely_invertible_elements : monoid → gr := λ X, carrierofasubsetwithbinop (submonoidtosubsetswithbinop _ (invertible_submonoid X)) ,, invertible_submonoid_grop X.
Require Import UniMath.MoreFoundations.Subtypes.