Lemma isaset_set_fun_space A (B : hSet) : isaset (A -> B). Proof. intros. change isaset with (isofhlevel 2). apply impred. apply (λ _, (pr2 B)). Qed.
Require Import UniMath.Foundations.UnivalenceAxiom.