proposition: Lemma iscoasymmquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : iscoasymm L) : iscoasymm (quotrel is).
proof: 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.
imports: UniMath.Foundations.Propositions