proposition: Lemma isapropiscomprelfun {X : UU} {Y : hSet} (R : hrel X) (f : X -> Y) : isaprop (iscomprelfun R f).
proof: Proof. apply impred. intro x. apply impred. intro x'. apply impred. intro r. apply Y. Defined.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets