Lemma weqhrelhrel0abmonoidfrac (X : abmonoid) (A : submonoid X) (iscanc : ∏ a : A, isrcancelable (@op X) (pr1carrier _ a)) (xa xa' : X × A) : (eqrelabmonoidfrac X A xa xa') ≃ (hrel0abmonoidfrac X A xa xa'). Proof. unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. apply weqimplimpl. apply (@hinhuniv _ (pr1 xa + pr1 (pr2 xa') = pr1 xa' + pr1 (pr2 xa))%logic). intro ae. induction ae as [ a eq ]. apply (invmaponpathsincl _ (iscanc a) _ _ eq). intro eq. apply hinhpr. exists (unel A). rewrite (runax X). rewrite (runax X). apply eq. apply (isapropishinh _). apply (setproperty X). Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.