Symmetric power functoriality is one of the basic cases of Langlands' functoriality conjectures and is the route to the proof of the Sato-Tate conjecture (concerning the distribution of the modulo p point counts of an elliptic curve over Q, as the prime p varies).   I will discuss the proof of the existence of the symmetric power liftings of Hilbert modular forms of regular weight. The proof uses automorphy lifting theorems, automorphic forms on unitary groups, and the geometry of Shimura varieties, as well as the fact that Spec Z is simply connected.   This is joint work with James Newton.