proposition: 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: Proof. intros. intros x x' r. apply ((pr1 (lg _ _)) (is _ _ r)). Defined.
imports: UniMath.Foundations.Propositions