Lemma isaset_set_sfun_space {S: UU} {X: sUU S} {Y: shSet S}: isaset (X s→ Y). Proof. change (isaset (X s→ Y)). apply impred_isaset. intros. apply isaset_forall_hSet. Defined.
Require Import UniMath.Foundations.All.