Lemma iscomprelfun2logeqf {X Y : UU} {L R : hrel X} (lg : hrellogeq L R) (f : X -> X -> Y) (is : iscomprelfun2 L f) : iscomprelfun2 R f. Proof. intros. intros x x' x0 x0' r r0. apply (is _ _ _ _ ((pr2 (lg _ _)) r) ((pr2 (lg _ _)) r0)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.