Created complete small category, and moved the proof of Freyd’s theorem to there from adjoint functor theorem.

]]>The (0,1)-category page says that a (0,1)-category “with the structure of a Grothendieck topos” is a locale, and a (0,1)-category “with the structure of an elementary topos” is a (complete?) Heyting algebra.

I am trying to understand the formal content of these statements. By the Giraud characterization of Grothendieck toposes, I could believe that (0,1)-categories which happen to be “Giraud toposes” (i.e., Grothendieck toposes) are locales. Running through the Giraud axioms, we have:

- “a locally small category with a small generating set” - should be true for any (0,1)-category
- “with all finite limits” - this means all finite meets for a (0,1)-category, which locales have
- “with all small coproducts, which are disjoint, and pullback stable” - for a (0,1) category, all small coproducts are small/infinitary disjunctions, and pullback stability corresponds to the “frame distributivity” rule which holds for locales, which says that binary meets distribute over joins. I’m not sure about the “disjoint” condition, though.
- “where all congruences have effective quotient objects, which are also pullback-stable.” I don’t understand.

But it does not seem that a (0,1)-category which is also an elementary topos is a complete Heyting algebra. The issue is that there is no subobject classifier. One reasons that the subobject classifier must be the terminal object of the cHa (it would be necessary to have a map into the subobject classifier from any object), but then since the pullback of every iso is an iso, every object must be the terminal object (Top), so the category is made only of terminal objects.

Is it in fact the case that a (0,1)-category which is a Grothendieck topos is a locale? And is there any *formal* way to view complete Heyting algebras as decategorified elementary toposes?