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