What is a reference for ["the equivalence between geometric theories and frames internal to the free topos"](https://indico.math.cnrs.fr/event/747/contributions/2523/attachments/1818/1962/introductionJoyal.pdf)? [1] This seems to be an extremely interesting theorem.


[1] André Joyal, “A crash course in topos theory: the big picture”, lectures at Topos à l'IHÉS, 2015.



Equivalence between geometric theories and frames internal to the free topos
Simon essentially answered the question already, but I will expand some of the parts that may not be clear to the experts. Sketches of an elephant is a good reference for everything I am going to say.
I will take a bit of a different narrative to Simon's, implicitly assuming a good understanding of classifying topoi, blurring the distinction between a topos and the geometric theory it classifies, $$\mathcal{E} \simeq \text{Set}[\mathbb{T}] .$$


**Def (Prebounds).** Let $\mathcal{E}$ be a topos. A *prebound* $e \in \mathcal{E}$ is an object such that the subobjects of its finite powers $m: a \to e^n$ are a generator for the topos. Such an object always exist and can be obtained by manipulating a generator (or a site).


**Construction (From prebounds to localic geometric morphisms).** Given a couple $(\mathcal{E},e)$ where $\mathcal{E}$ is a topos and $e$ is a prebound, we can construct a localic geometric morphism $$f\_e: \mathcal{E} \to \text{Set}[\mathbb{O}]. $$
Of course, this is the same of a cocontinuous left exact functor $f\_e^\*: \text{Set}[\mathbb{O}] \to \mathcal{E}$, which is the same of a lex functor $\text{Fin}^\circ \to \mathcal{E}$,


$$\text{Topoi}(\mathcal{E}, \text{Set}[\mathbb{O}]) \simeq \text{Cocontlex}( \text{Set}[\mathbb{O}], \mathcal{E}) \simeq \text{Cocontlex}( \text{Set}^{\text{Fin}}, \mathcal{E})\simeq \text{Lex}(\text{Fin}^\circ, \mathcal{E}). $$


The latter, is given by sending $n \mapsto e^n$. The geometric morphism obtained in this way is localic by definition of prebound. This construction appeared for the first time in **Freyd**'s *All topoi are localic*.


*Remark.* If you think about it, I am just spelling out in categorical terms what Simon suggested in somewhat mystical language.


*Remark (Morita-like phenomena)*. Notice that *each prebound* (and we can construct a prebound from any site) gives a different localic morphism, thus we have many localic representation for *the same* topos!


*Remark (Topoi are geometric theories, generators are their presentation)*. Following Thm 2.1.1 in **Caramello**'s *Theories, Sites, Toposes*, we see that a generator, or a site, is essentially the same of a linguistic presentation of the geometric theory classified by the topos.


**Theorem (Internal locales are localic geometric morphisms)**. There is a biequivalence of categories between the $2$-category of internal locales in $\text{Set}[\mathbb{O}]$ and the $2$-category of localic geometric morphisms over $\text{Set}[\mathbb{O}]$, $$\text{Loc}(\text{Set}[\mathbb{O}]) \leftrightarrows \text{Topoi}\_{\text{loc} / \text{Set}[\mathbb{O}]}. $$


*Proof.* Lemma 1.2 in **Johnstone**, *Factorization theorems for geometric morphisms*. Cahiers, 22, no1 (1981)


*Remark (On the emergence of Lawvere-like doctrines).* When one spells out what a locale internal to $ \text{Set}[\mathbb{O}]$ is, one discovers that it is nothing but a functor $$\mathbb{P}: \text{Fin} \to \text{Frames}$$ verifying the Beck-Chevalley condition and Frobenius reciprocity (see Lemma C.1.6.9 and Cor. C.1.6.10 in Sketches of an Elephant). Suddenly we see how doctrine-like objects emerge in the representation of theories! That's beautiful in my opinion. $\text{Fin}$ acts as a fact as a set of variables, while $\mathbb{P}(n)$ gives us the poset (a frame in fact) of formulas on those $n$-variables.


**Def (Well presented topoi).** The $2$-category WTopoi of *well presented topoi* has objects $(\mathcal{E},e)$ where $\mathcal{E}$ is a topos and $e$ is a prebound and morphism geometric morphisms whose left adjoint preserve the prebuound.


*Remark.* This notion does not appear in the literature (to my knowledge), I just need it as an intermediate notion. A good intuition for it is that the topos is specified together with a precise language generator of the geometric theory it classifies. WTopoi is really much more a $2$-category *of sites*, together with a *relational* notion of morphism of sites, rather than a $2$-category *of topoi*.


*Remark (Every topos can be well presented).* Of course, the WTopoi is not the same of Topoi but the forgetful functor $$\mathsf{U}: \text{WTopoi} \to \text{Topoi} $$ is essentially surjective on objects, and on morphisms (!).


**Theorem (Internal locales are well presented topoi and vice versa)**. There is a biequivalence of categories $$\text{Loc}(\text{Set}[\mathbb{O}]) \leftrightarrows \text{Topoi}\_{\text{loc} / \text{Set}[\mathbb{O}]} \leftrightarrows \text{WTopoi}.$$


