Lemma iscomprelrelif {X : UU} {R : hrel X} (L : hrel X) (isr : issymm R) (i1 : ∏ x x' y, R x x' -> L x y -> L x' y) (i2 : ∏ x y y', R y y' -> L x y -> L x y') : iscomprelrel R L. Proof. intros. intros x x' y y' rx ry. set (rx' := isr _ _ rx). set (ry' := isr _ _ ry). apply hPropUnivalence. - intro lxy. set (int1 := i1 _ _ _ rx lxy). apply (i2 _ _ _ ry int1). - intro lxy'. set (int1 := i1 _ _ _ rx' lxy'). apply (i2 _ _ _ ry' int1). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.