Added to *Set* the following remark:

“In constructive mathematics, $\mathcal{P}$ defines an equivalence of $\Set$ with the opposite category of that of complete atomic Heyting algebras. In fact, for any elementary topos $\mathcal{E}$, the power object functor defines an equivalence of $\mathcal{E}$ with the opposite category of that of internal complete atomic Heyting algebras. (This phrase can be interpreted using the internal language of $\mathcal{E}$.)”

Note that at *complete atomic Boolean algebra*, there is the following very interesting statement:

“This property of CABAs is not applicable in constructive mathematics, where power sets are rarely boolean algebras. However, we can use discrete locales instead (or rather, their corresponding frames). That is, define a **CABA** to be (not a complete atomic boolean algebra but) a frame $X$ such that the locale maps $X \to 1$ and $X \to X \times X$ (which in the category of frames are maps $0 \to X$ and $X + X \to X$) are open (as locale maps). Then it should be (I will check) a classical theorem that CABAs and complete atomic boolean algebras are the same, and a constructive theorem that CABAs and power sets are the same (in the same functorial manner as above).”

This is should really be checked someday. I will do it, but not now.

]]>Thanks!

The Definition-environment was supposed to be a Proposition-environment. I have changed it now. (This happens because I grab the code for these environments from the Instiki-Theorems page where it is the Definition-environment that is written out. Here I forgot to edit it after copy-and-pasting.)

]]>I sharpened Urs’s paragraph. Incidentally, I didn’t understand why this was cast in a definition environment (definition 1).

]]>added to *Set* a brief paragraph *Set -- Properties -- Opposite category and Boolean algebras*

In general I think it's more common to name functors after what they do to objects, not to the elements of those objects

Here is an idea: would it help if I write systematically?

]]>I think there are some level-type conflations here. The constant stack with fibre the groupoid Set is the stack of locally constant sheaves. The constant sheaf with fibre F is the sheaf of locally constant functions with values in F.

]]>I just find it confusing to write "LConst" for the functor which constructs constant sheaves -- my mind keeps trying to read it as a functor which constructs locally constant sheaves. In general I think it's more common to name functors after what they do to objects, not to the elements of those objects. For instance, we say "the free monoid functor" not "the words functor," and "the free strict oo-category functor" not "the pasting diagrams functor." Probably you agree that the functor is "the constant sheaf functor," but then I think the notation of the functor should reflect the name of the functor.

]]>should be the constant sheaf on .

Well, it's called the "constant sheaf" of course. I still found it a great idea to write for the constant sheaf on . Originally I kept writing with a little space to amplify that it is the sheafification of the constant presheaf. Then it seemed like a neat idea to just discard the space.

I think it fits nicely into the pattern. This way for instance we have precisely that is the set of locally constant functions.

More generally, for the constant -stack on the n-groupoid of (n-1)-groupoids, we have

is precisely the n-groupoid of locally constant (n-1)-stacks. So that works very nicely. If I write instead of here a very nice abstract pattern is severely broken by the notation.

Or so I think.

]]>Hmm, I guess I see that, but my intuition is that Const(X) should be the constant sheaf on X.

]]>Why is the left adjoint in that section called "LConst" rather than "Const"?

For two reasons:

is the constant sheaf of locally constant functions! The sheaf is named after what it is "a sheaf of".

for a site, the functor should be called . Then with the geometric embedding, we have the pleasant

Why is the left adjoint in that section called "LConst" rather than "Const"?

]]>hm, but then I have a mistake in the section global section functor on a general topos...

]]>Ah, right. Thanks.

]]>I added the modifier 'Grothendieck' to topos, since for example there is no geometric morphism .

]]>added to Set the statement that is the terminal topos.

]]>