Lemma isantisymmnegquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : isantisymmneg L) : isantisymmneg (quotrel is). Proof. intros. unfold isantisymmneg. assert (int : ∏ (x1 x2 : setquot R), isaprop (neg (quotrel is x1 x2) -> neg (quotrel is x2 x1) -> x1 = x2)). { intros x1 x2. apply impred. intro. apply impred. intro. apply (isasetsetquot R x1 x2). } apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))). intros x x'. intros r r'. apply (maponpaths (setquotpr R) (isl x x' r r')). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.