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