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