Definition weqabgrdiff (X : abmonoid) : weq (abgrdiff X) (abmonoidfrac X (totalsubmonoid X)). Proof. intros. apply (weqsetquotweq (eqrelabgrdiff X) (eqrelabmonoidfrac X (totalsubmonoid X)) (weqabgrdiffint X)). - simpl. intros x x'. induction x as [ x1 x2 ]. induction x' as [ x1' x2' ]. simpl in *. apply hinhfun. intro tt0. induction tt0 as [ xx0 is0 ]. exists (make_carrier (λ x : X, htrue) xx0 tt). apply is0. - simpl. intros x x'. induction x as [ x1 x2 ]. induction x' as [ x1' x2' ]. simpl in *. apply hinhfun. intro tt0. induction tt0 as [ xx0 is0 ]. exists (pr1 xx0). apply is0. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.