Lemma setquotuniv_equal { X : UU } ( R : hrel X ) ( Y : hSet ) ( f f' : X -> Y ) (p : f = f') ( is : iscomprelfun R f ) ( is' : iscomprelfun R f' ) : setquotuniv R Y f is = setquotuniv R Y f' is'. Proof. intros. destruct p. apply funextsec; intro c. assert(ip : isaprop (iscomprelfun R f)). { apply impred; intro x; apply impred; intro x'. apply impred; intro p. apply setproperty. } assert( q : is = is' ). { apply ip. } destruct q. reflexivity. Qed.
Require Import