Lemma iscomprelrelfun2if {X Y : UU} (RX : hrel X) (RY : eqrel Y) (f : X -> X -> Y) (is1 : ∏ x x' x0 : X, RX x x' -> RY (f x x0) (f x' x0)) (is2 : ∏ x x0 x0' : X, RX x0 x0' -> RY (f x x0) (f x x0')) : iscomprelrelfun2 RX RY f. Proof. intros. intros x x' x0 x0'. intros r r'. set (e := is1 x x' x0 r). set (e' := is2 x' x0 x0' r'). apply (eqreltrans RY _ _ _ e e'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.