Lemma isreflquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : isrefl L) : isrefl (quotrel is). Proof. intros. unfold isrefl. apply (setquotunivprop R). intro x. apply (isl x). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.