Topos-theoretic Galois theory This page is an overview of some of the types of "Galois theories" there are. One of the most basic type is the fundamental theorem of covering spaces, which says, roughly, that for each topological space $X$, there is an equivalence of categories
$$\mathrm{Cov}(X)\simeq \pi_1(X)\mathbf{Set}.$$
Grothendieck proved an analogue of that statement for schemes $X$:
$$\mathrm{EtCov}(X)\simeq \pi_1(X)\mathbf{Set}.$$
(This is again just a very rough formulation and omits some of the assumptions, but you know what I mean.)
I am interested in "topos-theoretic Galois theory". Unfortunately, this section of the nLab page isn't filled out ("(...)"), but I guess that the topos-theoretic formulation of Galois theory states, roughly, that for each topos $\mathcal E$,
$$\mathrm{Gal}(\mathcal E)\simeq \pi_1(\mathcal E)\mathbf{Set},\qquad (\ast)$$
where $\mathrm{Gal}(\mathcal E)$ is the full subcategory of $\mathcal E$ consisting of locally constant objects in $\mathcal E$, and $\pi_1(\mathcal E)$ is the fundamental group of $\mathcal E$. (This is suggested by the nLab section "Reformulation of classical Galois theory".)
Question: Is there a reference for $(\ast)$ (and the definition of the fundamental group of a topos which is used here)? Is this in SGA 4?
The linked nLab page fundamental group of a topos refers to (and is mostly copy-pasted from) Porter's paper Abstract Homotopy Theory: The interaction of category theory and homotopy theory, which contains a section called "The fundamental group of a topos", which in turn refers to SGA 1. This is weird, because SGA 1 doesn't discuss topoi, so in particular not the fundamental group of a topos!
The nLab also refers to SGA 4 Exposé IV Exercice 2.7.5 for the definition of the fundamental group and SGA 4 Exposé VIII Proposition 2.1 for, I guess, $(\ast)$ in the special case that $\mathcal E$ is the étale topos of the scheme $X=\mathrm{Spec}(k)$ for some field $k$. (But this is really just a guess - I can't read French. So correct me if I'm wrong.) Is there more of "topos-theoretic Galois theory" in SGA 4 or are these the only two paragraphs about that topic?
Concerning the definition of the fundamental group of a topos, there is a construction in Moerdijk's Classifying Spaces and Classifying Topoi, in which he nevertheless remarks:

The profinite fundamental group is discussed in
SGA1.

This suggests there are two version of the fundamental group of a topos: the one he discusses and the "profinite" version. However, as I said, topoi don't occur in SGA 1, so I wonder where I can find the definition of the "profinite" fundamental group, if that's the notion that should be used in $(\ast)$. (The definition used in $(\ast)$ should of course have the property that if $\mathcal E$ is the étale topos of a scheme $X$, then $\pi_1(\mathcal E)$ is isomorphic to the étale fundamental group of $X$.)
 A: Maybe you would like to see the thesis of O. Leroy, Groupoïde fondamental et théorème de Van Kampen en théorie des topos, available from https://plmbox.math.cnrs.fr/f/7ffa366379144dd4bacc/?dl=1 — the password is : groupoide
(a project of transcription)

or the thesis of V. Zoonekynd, La Tour de Teichmuller-Grothendieck, available from https://tel.archives-ouvertes.fr/tel-00001140/document
A: I believe that chapter $5$ of Galois Theories by Borceux and Janelidze contains what you're looking for -- they develop a general 'categorical Galois theorem' invoking toposes.
Chapter 7 gets even more general, presenting a 'non-Galoisian Galois theorem' that holds for any descent morphism in a category -- a morphism $f$ is a descent morphism iff the 'pullback along $f$' functor is monadic.
There is also the classic paper by Joyal and Tierney, An Extension of the Galois theory of Grothendieck, where they prove that each Grothendieck topos is equivalent to the category of equivariant sheaves on a groupoid internal to the category of locales.
This paper by Christopher Townsend might be of interest to your specific question; he re-proves Joyal and Tierney’s result on the representation of Grothendieck toposes as localic groupoids using a simplified case of the aforementioned categorical Galois theorem, then proceeds to actually prove the whole theorem using this trivial case as a key ingredient.
