X n : power_iterated (X -> HProp) n = (power_iterated X n -> HProp) := (nat_iter_succ_r _ _ _)^. Global Instance hset_power {UA : Univalence} (X : HSet) : IsHSet (X -> HProp). Proof. apply istrunc_S. intros p q. apply hprop_allpath. intros H H'. destruct (equiv_path_arrow p q) as [f [g Hfg Hgf _]]. rewrite <- (Hfg H), <- (Hfg H'). apply ap. apply path_forall. intros x. apply path_ishprop. Qed.
From HoTT Require Import Basics Types TruncType. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card Spaces.Nat.Core.