Definition logeqabgrdiffrels (X : abmonoid) {L : hrel X} (is : isbinophrel L) : hrellogeq (abgrdiffrel' X is) (abgrdiffrel X is). Proof. intros x1 x2. split. - assert (int : ∏ x x', isaprop (abgrdiffrel' X is x x' → abgrdiffrel X is x x')). { intros x x'. apply impred. intro. apply (pr2 _). } generalize x1 x2. clear x1 x2. apply (setquotuniv2prop _ (λ x x', make_hProp _ (int x x'))). intros x x'. change ((abgrdiffrelint' X L x x') → (abgrdiffrelint _ L x x')). apply (pr1 (logeqabgrdiffrelints X L x x')). - assert (int : ∏ x x', isaprop (abgrdiffrel X is x x' → abgrdiffrel' X is x x')). intros x x'. apply impred. intro. apply (pr2 _). generalize x1 x2. clear x1 x2. apply (setquotuniv2prop _ (λ x x', make_hProp _ (int x x'))). intros x x'. change ((abgrdiffrelint X L x x') → (abgrdiffrelint' _ L x x')). apply (pr2 (logeqabgrdiffrelints X L x x')). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.