Return to Answer

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{Heyt}$$ 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 set of formulas on those $n$-variables.

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.

Theorem (Internal locales are localic geometric morphisms). There is a biequivalence of categories between the $2$-category of internal locales in $\text{Loc}(\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}]}. $$

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}]}. $$

Theorem (Internal locales are localic geometric morphisms). There is a biequivalence of categories between the $2$-category of internal locales in $\text{Loc}(\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}]}. $$

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{Loc}(\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}]}. $$