Definition invertible_submonoid (X : monoid) : @submonoid X. Proof. refine (merely_invertible_elements (@op X) (pr2 X),, _). split. - intros xpair ypair. apply mere_invop. + exact (pr2 xpair). + exact (pr2 ypair). - apply hinhpr; exact (1 ,, (lunax _ 1) ,, (lunax _ 1)). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.