proposition: Lemma fun_equiv_isfun `{Univalence} {A B : Type} : (A -> B) <~> {R : A -> B -> Type | IsFun R}.
proof: Proof. have fe : Funext by apply: Univalence_implies_Funext. transitivity (A -> {P : B -> Type | Contr {y : B & P y}}). { apply: equiv_postcompose'; exact type_equiv_contr. } by apply (equiv_composeR' (equiv_sig_coind _ _)^-1). Defined.
imports: Coq(ssreflect)