One can think of locales as (generalizations of) topological spaces which don't necessary have (enough) points. Of course when one studies locales, one "actually" studies frames, certain sorts of lattices, but reverses the arrows so that story has a less algebraic and more geometrical/topological flavor.

So while "localic spaces" make lack for a "sufficient" *set* of point, by their very nature they do have a sufficient *set* of "open sets" (scare quotes because these open sets arise as a primitive notion and not as actual sets of anything).

Curiosity drive us on: could one go a step further and make the open sets of locales as ghostly as locales make the points of spaces ghostly?

Let me put the question more technically (but correct me if you think now that I'm asking the wrong question): One often interprets algebraic objects such as "group objects" in sufficiently nice categories. So locales with ghostly open sets might show up as localic locales, or what amounts to the same, "coframic frames" -- diagrams in the opposite category to the category of frames, specifically diagrams that define internal frames. Though such things must have at least two points (the empty set and the total space) corresponding to the nullary operations in the algebraic theory (just as a localic group must have at least one point, the identity, a priori it seems that they might have no more.

In this spirit

How would one construct interesting examples of coframic frames = localic locales?

Even if such things have few classical points, and few classical open sets, they will still have plenty of classical (open) sets of open sets.

By what formalism might one keep on going, iterating the internalization?

The previous question implicitly suggests levels of internalization indexed by natural numbers?

Could someone propose a definition for a level of internalization indexed by a limit ordinal?

spacerather than asetof "open sets", sure, but I don't see immediately what the correct axioms are. Maybe there are some good ones --- instead of demanding that the union of any collection of open sets be open, I could demand this only for open collections of open sets? Instead of the "finiteset" rule for intersections, perhaps I'm allowed to intersect anycompactcollection of opens? $\endgroup$ – Theo Johnson-Freyd Feb 6 '11 at 6:15Ifeel more secure internalizing algebraic theories in a nice category and more general notions (like topology). For example, I understand topological groups as group objects in the category of topological spaces, but I'm not exactly sure what I topological space object in the category of groups might mean. Likewise, the notion of a topological frame seems immediately clear and unambiguous, and I guess one could also call such a thing a topological locale or spatial locale. Splits our difference. $\endgroup$ – David Feldman Feb 6 '11 at 8:56