proposition: Lemma isaset_set_sfun_space {S: UU} {X: sUU S} {Y: shSet S}: isaset (X s→ Y).
proof: Proof. change (isaset (X s→ Y)). apply impred_isaset. intros. apply isaset_forall_hSet. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.HVectors