Lemma isgropif {X : hSet} {opp : binop X} (is0 : ismonoidop opp) (is : ∏ x : X, merely_hasrinv opp is0 x) : isgrop opp. Proof. exists is0. induction is0 as [ assoc isun0 ]. induction isun0 as [ un0 unaxs0 ]. simpl in is. simpl in unaxs0. simpl in un0. simpl in assoc. simpl in unaxs0. assert (l1 : ∏ x' : X, isincl (λ x0 : X, opp x0 x')). { intro x'. apply (@hinhuniv (∑ (x0 : X), opp x' x0 = un0) (make_hProp _ (isapropisincl (λ x0 : X, opp x0 x')))). - intro int1. simpl. apply isinclbetweensets. + apply (pr2 X). + apply (pr2 X). + intros a b. intro e. rewrite <- (pr2 unaxs0 a). rewrite <- (pr2 unaxs0 b). induction int1 as [ invx' eq ]. rewrite <- eq. induction (assoc a x' invx'). induction (assoc b x' invx'). rewrite e. apply idpath. - apply (is x'). } assert (is' : ∏ x : X, ∃ (x0 : X), opp x0 x = un0). { intro x. apply (λ f , hinhuniv f (is x)). intro s1. induction s1 as [ x' eq ]. apply hinhpr. exists x'. simpl. apply (invmaponpathsincl _ (l1 x')). rewrite (assoc x' x x'). rewrite eq. rewrite (pr1 unaxs0 x'). unfold unel_is. simpl. rewrite (pr2 unaxs0 x'). apply idpath. } assert (l1' : ∏ x' : X, isincl (λ x0 : X, opp x' x0)). { intro x'. apply (@hinhuniv (∑ (x0 : X), opp x0 x' = un0) (make_hProp _ (isapropisincl (λ x0 : X, opp x' x0)))). - intro int1. simpl. apply isinclbetweensets. + apply (pr2 X). + apply (pr2 X). + intros a b. intro e. rewrite <- (pr1 unaxs0 a). rewrite <- (pr1 unaxs0 b). induction int1 as [ invx' eq ]. rewrite <- eq. induction (!assoc invx' x' a). induction (!assoc invx' x' b). rewrite e. apply idpath. - apply (is' x'). } assert (int : ∏ x : X, isaprop (∑ (x0 : X), opp x0 x = un0)%logic). { intro x. apply isapropsubtype. intros x1 x2. intros eq1 eq2. apply (invmaponpathsincl _ (l1 x)). rewrite eq1. rewrite eq2. apply idpath. } simpl. set (linv0 := λ x : X, hinhunivcor1 (make_hProp _ (int x)) (is' x)). simpl in linv0. set (inv0 := λ x : X, pr1 (linv0 x)). exists inv0. simpl. exists (λ x, pr2 (linv0 x)). intro x. apply (invmaponpathsincl _ (l1 x)). rewrite (assoc x (inv0 x) x). change (inv0 x) with (pr1 (linv0 x)). rewrite (pr2 (linv0 x)). unfold unel_is. simpl. rewrite (pr1 unaxs0 x). rewrite (pr2 unaxs0 x). apply idpath. Defined.