proposition: Lemma isirreflquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : isirrefl L) : isirrefl (quotrel is).
proof: Proof. intros. unfold isirrefl. apply (setquotunivprop R (λ x, make_hProp _ (isapropneg (quotrel is x x)))). intro x. apply (isl x). Defined.
imports: UniMath.Foundations.Propositions