proposition: Lemma isgropif {X : hSet} {opp : binop X} (is0 : ismonoidop opp) (is : ∏ x : X, merely_hasrinv opp is0 x) : isgrop opp.
proof: Proof. split with is0. destruct is0 as [ assoc isun0 ]. destruct 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 (total2 (λ 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 (pathsinv0 (pr2 unaxs0 a)). rewrite (pathsinv0 (pr2 unaxs0 b)). destruct int1 as [ invx' eq ]. rewrite (pathsinv0 eq). destruct (assoc a x' invx'). destruct (assoc b x' invx'). rewrite e. apply idpath. - apply (is x'). } assert (is' : ∏ x : X, hexists (λ x0 : X, (opp x0 x) = un0)). { intro x. apply (λ f : _ , hinhuniv f (is x)). intro s1. destruct s1 as [ x' eq ]. apply hinhpr. split with 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 (total2 (λ 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 (pathsinv0 (pr1 unaxs0 a)). rewrite (pathsinv0 (pr1 unaxs0 b)). destruct int1 as [ invx' eq ]. rewrite (pathsinv0 eq). destruct (pathsinv0 (assoc invx' x' a)). destruct (pathsinv0 (assoc invx' x' b)). rewrite e. apply idpath. - apply (is' x'). } assert (int : ∏ x : X, isaprop (total2 (λ x0 : X, (opp x0 x) = un0))). { 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)). split with inv0. simpl. split with (λ 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions