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