Theorem impredtech1 (n : nat) (X Y : UU) : (X -> isofhlevel n Y) -> isofhlevel n (X -> Y). Proof. revert X Y. induction n as [ | n IHn ]. intros X Y X0. simpl. split with (λ x, pr1 (X0 x)). - intro t. assert (s1 : ∏ x, t x = pr1 (X0 x)) by (intro; apply proofirrelevancecontr; apply (X0 x)). apply funextsec. assumption. - intros X Y X0. simpl. assert (X1 : X -> isofhlevel (S n) (X -> Y)) by (intro X1; apply impred; assumption). intros x x'. assert (s1 : isofhlevel n (∏ xx, x xx = x' xx)) by (apply impred; intro t; apply (X0 t)). assert (w : (∏ xx, x xx = x' xx) ≃ (x = x')) by apply (weqfunextsec _ x x'). apply (isofhlevelweqf n w s1). Defined.