proposition: Lemma funspace_isaset {X Y} : isaset Y -> isaset (X -> Y).
proof: Proof. intros is. apply (impredfun 2). assumption. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions