proposition: Lemma invertibilityinabmonoidfrac (X : abmonoid) (A : submonoid X) : ∏ a a' : A, isinvertible (@op (abmonoidfrac X A)) (prabmonoidfrac X A (pr1 a) a').
proof: 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 : _, paths (g (f x0)) x0). { apply (setquotunivprop R (λ x, _ = _)). intro xb. simpl. apply (iscompsetquotpr R (@make_dirprod X A ((pr1 a') + ((pr1 a) + (pr1 xb))) ((@op A) a ((@op A) a' (pr2 xb))))). simpl. apply hinhpr. split with (unel A). unfold pr1carrier. simpl. set (e := assocax X (pr1 a) (pr1 a') (pr1 (pr2 xb))). simpl in e. destruct e. set (e := assocax X (pr1 xb) (pr1 a + pr1 a') (pr1 (pr2 xb))). simpl in e. destruct e. set (e := assocax X (pr1 a') (pr1 a) (pr1 xb)). simpl in e. destruct e. set (e := commax X (pr1 a) (pr1 a')). simpl in e. destruct e. set (e := commax X (pr1 a + pr1 a') (pr1 xb)). simpl in e. destruct e. apply idpath. } assert (efg : ∏ x0 : _, paths (f (g x0)) x0). { apply (setquotunivprop R (λ x0, _ = _)). intro xb. simpl. apply (iscompsetquotpr R (@make_dirprod X A ((pr1 a) + ((pr1 a') + (pr1 xb))) ((@op A) a' ((@op A) a (pr2 xb))))). simpl. apply hinhpr. split with (unel A). unfold pr1carrier. simpl. set (e := assocax X (pr1 a') (pr1 a) (pr1 (pr2 xb))). simpl in e. destruct e. set (e := assocax X (pr1 xb) (pr1 a' + pr1 a) (pr1 (pr2 xb))). simpl in e. destruct e. set (e := assocax X (pr1 a) (pr1 a') (pr1 xb)). simpl in e. destruct e. set (e := commax X (pr1 a') (pr1 a)). simpl in e. destruct e. set (e := commax X (pr1 a' + pr1 a) (pr1 xb)). simpl in e. destruct e. apply idpath. } apply (isweq_iso _ _ egf efg). } apply (make_dirprod isl (weqlinvertiblerinvertible (@op (abmonoidfrac X A)) (commax (abmonoidfrac X A)) (prabmonoidfrac X A (pr1 a) a') isl)). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders