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