Return to Answer

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want (so in particular, you can emulate function symbol using functional relations).

So frames in the free topos corresponds exactly to one-sorted geometric theory (with propositions and functions). In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But if you look in P.T.Johnstone Sketches of an elephant, you should find a good approximation to it as Theorem D3.2.5. The theorem might not be exaclty what you are after, but it contains all the key elements.

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want (so in particular, you can emulate function symbol using functional relations).

So frames in the free topos corresponds exactly to one-sorted geometric theory (with propositions and functions). In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But if you look in P.T.Johnstone Sketches of an elephant, you should find a good approximation to it as Theorem D3.2.5. The theorem might not be exactly what you are after, but it contains all the key elements. (Also using that localic geometric morphisms corresponds to internal frames of course)

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want (so in particular, you can emulate function symbol using functional relations).

So frames in the free topos corresponds exactly to one-sorted geometric theory (with propositions and functions). In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But you should find in the Elephant (I'll add a more precise reference later today - I don't have the book with me right now) a proof that every Grothendieck topos admits a localic geometric morphisms to the Free topos, which should give you a decent idea of how things works : interpreted in terms of classyfing topos this corresponds to the joint observation that every geometric theory is Morita equivant to one corresponding to a frame in the Free topos. So looking at the details of the proof should clarify this, at least if your fluent in the "Geometric Theory-Classifying topos" translation.

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want (so in particular, you can emulate function symbol using functional relations).

So frames in the free topos corresponds exactly to one-sorted geometric theory (with propositions and functions). In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But if you look in P.T.Johnstone Sketches of an elephant, you should find a good approximation to it as Theorem D3.2.5. The theorem might not be exaclty what you are after, but it contains all the key elements.

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many geometric axioms as you want.

So frames in the free topos corresponds exactly to one-sorted geometric theory. In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But you should find in the Elephant (I'll add a more precise reference later today - I don't have the book with me right now) a proof that every Grothendieck topos admits a localic geometric morphisms to the Free topos, which should give you a decent idea of how things works : interpreted in terms of classyfing topos this corresponds to the joint observation that every geometric theory is Morita equivant to one corresponding to a frame in the Free topos. So looking at the details of the proof should clarify this, at least if your fluent in the "Geometric Theory-Classifying topos" translation.

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want (so in particular, you can emulate function symbol using functional relations).

So frames in the free topos corresponds exactly to one-sorted geometric theory (with propositions and functions). In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But you should find in the Elephant (I'll add a more precise reference later today - I don't have the book with me right now) a proof that every Grothendieck topos admits a localic geometric morphisms to the Free topos, which should give you a decent idea of how things works : interpreted in terms of classyfing topos this corresponds to the joint observation that every geometric theory is Morita equivant to one corresponding to a frame in the Free topos. So looking at the details of the proof should clarify this, at least if your fluent in the "Geometric Theory-Classifying topos" translation.