Lemma iscomprelrelfun2logeqf2 {X Y : UU} (RX : hrel X) {LY RY : hrel Y} (lg : hrellogeq LY RY) (f : X -> X -> Y) (is : iscomprelrelfun2 RX LY f) : iscomprelrelfun2 RX RY f. Proof. intros. intros x x' x0 x0' r r0. apply ((pr1 (lg _ _)) (is _ _ _ _ r r0)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.