Theorem weqfromfunstntostn ( n m : nat ) : (⟦n⟧ -> ⟦m⟧) ≃ ⟦natpower m n⟧. Proof. revert m. induction n as [ | n IHn ]. - intro m. apply weqcontrcontr. + apply ( iscontrfunfromempty2 _ weqstn0toempty ). + apply iscontrstn1. - intro m. set ( w1 := weqfromcoprodofstn 1 n ). assert ( w2 : ( ⟦S n⟧ -> ⟦m⟧ ) ≃ ( (⟦1⟧ ⨿ ⟦n⟧) -> ⟦m⟧ ) ) by apply ( weqbfun _ w1 ). set ( w3 := weqcomp w2 ( weqfunfromcoprodtoprod (⟦1⟧) (⟦n⟧) (⟦m⟧) ) ). set ( w4 := weqcomp w3 ( weqdirprodf ( weqfunfromcontr (⟦m⟧) iscontrstn1 ) ( IHn m ) ) ). apply ( weqcomp w4 ( weqfromprodofstn m ( natpower m n ) ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.