proposition: Lemma weqhrelhrel0abmonoidfrac (X : abmonoid) (A : submonoid X) (iscanc : ∏ a : A, isrcancelable (@op X) (pr1carrier _ a)) (xa xa' : dirprod X A) : (eqrelabmonoidfrac X A xa xa') ≃ (hrel0abmonoidfrac X A xa xa').
proof: Proof. unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. apply weqimplimpl. apply (@hinhuniv _ (pr1 xa + pr1 (pr2 xa') = pr1 xa' + pr1 (pr2 xa))). intro ae. destruct ae as [ a eq ]. apply (invmaponpathsincl _ (iscanc a) _ _ eq). intro eq. apply hinhpr. split with (unel A). rewrite (runax X). rewrite (runax X). apply eq. apply (isapropishinh _). apply (setproperty X). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders