This question is about Joyal and Tierney's famous *An extension of the Galois theory of Grothendieck*. One of the main results states (see the MathSciNet review by Peter Johnstone):

**Joyal and Tierney's theorem.** *Each Grothendieck topos is equivalent to the topos of equivariant sheaves on a groupoid in the category of locales.*

**Question 1.** What does this statement have to do with Grothendieck's Galois theory?

I have to admit, I don't know much about Grothendieck's Galois theory and which kind of theorems it includes. In my mind, I usually identify the term "Grothendieck's Galois theory" with the following theorem (see Chua - The étale fundamental group for a concise introduction and SGA 1 for a complete treatment):

**Grothendieck's theorem.** *Let $X$ be a scheme and $x\in X$. Then the category of finite étale covers of $X$ is equivalent to the category of finite continuous $\pi_1(X,x)$-sets, where $\pi_1(X,x)$ is the étale fundamental group of $X$ at the base point $x$.*

This is related to Galois theory because whenever $k$ is a field, then the étale fundamental group of $\operatorname{Spec}(k)$ is the absolute Galois group of $k$.

A more precise version of Question 1 would be: does Joyal and Tierney's theorem imply Grothendieck's theorem? (But an answer showing that Joyal and Tierney's theorem implies a modified version of Grothendieck's theorem would satisfy me as well.)

**Question 2.** In an answer by Zhen Lin to "What does a proof in an internal logic actually look like?" it is mentioned that the proof of Joyal and Tierney's theorem uses the internal language of toposes. In which way does it use the internal language? Which kind of theorems are proved internally, how are they interpreted externally, and why are the external interpretations of these theorems helpful in proving Joyal and Tierney's theorem? Skimming the text I don't see any logic at all.