Existence of harmonic maps into CAT(1) spaces

Let $\varphi\in C^0 \cap W^{1,2}(\Sigma, X)$ where $\Sigma$ is a compact Riemann surface, $X$ is a compact locally CAT(1) space, and $W^{1,2}(\Sigma,X)$ is defined as in Korevaar-Schoen. We use the technique of harmonic replacement to prove that either there exists a harmonic map $u:\Sigma \to X$ homotopic to $\varphi$ or there exists a conformal harmonic map $v:\mathbb S^2 \to X$. To complete the argument, we prove compactness for energy minimizers and a removable singularity theorem for conformal harmonic maps.