Lemma weqhrelhrel0commringfrac (X : commring) (S : @submonoid (ringmultabmonoid X)) (iscanc : ∏ a : S, isrcancelable (@op2 X) (pr1carrier _ a)) (xa xa' : X × S) : (eqrelcommringfrac X S xa xa') ≃ (hrelcommringfrac0 X S xa xa'). Proof. intros. unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. apply weqimplimpl. - apply (@hinhuniv _ (_ = _)). intro ae. induction ae as [ a eq ]. apply (invmaponpathsincl _ (iscanc a) _ _ eq). - intro eq. apply hinhpr. exists (unel S). rewrite (ringrunax2 X). rewrite (ringrunax2 X). apply eq. - apply (isapropishinh _). - apply (setproperty X). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.