Definition iscomprelrelfun2 {X Y : UU} (RX : hrel X) (RY : hrel Y) (f : X -> X -> Y) : UU := ∏ x x' x0 x0' : X, RX x x' -> RX x0 x0' -> RY (f x x0) (f x' x0').
Require Import UniMath.Foundations.UnivalenceAxiom.