Lemma ispoquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : ispreorder L) : ispreorder (quotrel is). Proof. intros. split with (istransquotrel is (pr1 isl)). apply (isreflquotrel is (pr2 isl)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.