You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Callan McGill (Aug 08 2022 at 21:35):I've been thinking recently about how the "fundamental theorem of topos theory" looks from the POV of locales. Suppose L is a locale. Then we can show that for any a ∈ L that the downset ↓ a forms a locale also. Moreover, if we have a ≤ b then we get a geometric morphism ↓ a -> ↓ b where the pullback is described by just taking the meet with a. One way to package up that information is to say something like: The codomain fibration is "localic" (made up terminology) meaning that the fibers are locales and cartesian maps preserve the structure. I am wondering if there is any way to make this picture 2-categorical on the entire category of Locales in the sense that we have a fibration associated to each locale but I am unsure if we can say something about that structure when we add locale morphisms.