Lemma invertibilityinabmonoidfrac (X : abmonoid) (A : submonoid X) : ∏ a a' : A, isinvertible (@op (abmonoidfrac X A)) (prabmonoidfrac X A (pr1 a) a'). Proof. intros a a'. set (R := eqrelabmonoidfrac X A). unfold isinvertible. assert (isl : islinvertible (@op (abmonoidfrac X A)) (prabmonoidfrac X A (pr1 a) a')). { unfold islinvertible. set (f := λ x0 : abmonoidfrac X A, prabmonoidfrac X A (pr1 a) a' + x0). set (g := λ x0 : abmonoidfrac X A, prabmonoidfrac X A (pr1 a') a + x0). assert (egf : ∏ x0, g (f x0) = x0). { apply (setquotunivprop R (λ x, _ = _)%logic). intro xb. simpl. apply (iscompsetquotpr R (pr1 a' + (pr1 a + pr1 xb) ,, (@op A) a ((@op A) a' (pr2 xb)))). simpl. apply hinhpr. exists (unel A). unfold pr1carrier. simpl. set (e := assocax X (pr1 a) (pr1 a') (pr1 (pr2 xb))). simpl in e. induction e. set (e := assocax X (pr1 xb) (pr1 a + pr1 a') (pr1 (pr2 xb))). simpl in e. induction e. set (e := assocax X (pr1 a') (pr1 a) (pr1 xb)). simpl in e. induction e. set (e := commax X (pr1 a) (pr1 a')). simpl in e. induction e. set (e := commax X (pr1 a + pr1 a') (pr1 xb)). simpl in e. induction e. apply idpath. } assert (efg : ∏ x0, f (g x0) = x0). { apply (setquotunivprop R (λ x0, _ = _)%logic). intro xb. simpl. apply (iscompsetquotpr R (pr1 a + (pr1 a' + pr1 xb) ,, (@op A) a' ((@op A) a (pr2 xb)))). simpl. apply hinhpr. exists (unel A). unfold pr1carrier. simpl. set (e := assocax X (pr1 a') (pr1 a) (pr1 (pr2 xb))). simpl in e. induction e. set (e := assocax X (pr1 xb) (pr1 a' + pr1 a) (pr1 (pr2 xb))). simpl in e. induction e. set (e := assocax X (pr1 a) (pr1 a') (pr1 xb)). simpl in e. induction e. set (e := commax X (pr1 a') (pr1 a)). simpl in e. induction e. set (e := commax X (pr1 a' + pr1 a) (pr1 xb)). simpl in e. induction e. apply idpath. } apply (isweq_iso _ _ egf efg). } exact ( isl ,, weqlinvertiblerinvertible op (commax (abmonoidfrac X A)) (prabmonoidfrac X A (pr1 a) a') isl ). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.