Lemma iscomprelfunlogeqf1 {X Y : UU} {LX RX : hrel X} (RY : hrel Y) (lg : hrellogeq LX RX) (f : X -> Y) (is : iscomprelrelfun LX RY f) : iscomprelrelfun RX RY f. Proof. intros. intros x x' r. apply (is _ _ (pr2 (lg _ _) r)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.