Lemma iscomprelfun2if {X Y : UU} (R : hrel X) (f : X -> X -> Y) (is1 : ∏ x x' x0 : X, R x x' -> f x x0 = f x' x0) (is2 : ∏ x x0 x0' : X, R x0 x0' -> f x x0 = f x x0') : iscomprelfun2 R 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 (pathscomp0 e e'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.