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