Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added a comment to the end of the discussion at predicative mathematics to the effect that free small-colimit completions of toposes are examples of locally cartesian closed pretoposes that are generally not toposes.
In fact, there could be some interesting stability theorems here. For one, if is a complete and cocomplete -pretopos, then we have an evident functor and I believe
(Note: it may be shown that , for an -lextensive category, is the free small-coproduct completion of .) Furthermore, if denotes the ex/lex completion, then
One import of this is that the free small-colimit completion , for a complete and cocomplete -pretopos, is equivalent to , which by the above is also a complete and cocomplete -pretopos.
Furthermore, I conjecture that the above stability theorems carry over to --pretoposes in place of -pretoposes. These constructions seem to give interesting ways of constructing lots of non-topos examples.
Cool!
If you have a left exact (or even pullback-preserving) comonad on a pretopos, is the category of coalgebras also a pretopos? Same question for -pretoposes.
My question in 4 is in fact an incredibly easy ’yes’ (on both counts). Well, certainly the pretopos part is: all the axioms of a pretopos are in terms of colimits and pullbacks. If is a pullback-preserving comonad, then the underlying functor preserves and reflects colimits and pullbacks, and this means that the pretopos axioms hold on if they hold on . Nothing could be simpler.
(It makes me suspect that a very easy conceptual proof of the lex comonad theorem for toposes might be available if we ’define’ a topos to be a lex total category, which is not too far off from the truth for Grothendieck toposes.)
The analogous result for -pretoposes is also pretty easy if you quote the result (say from the Elephant) that if is locally cartesian closed, then so is . (I am defining a -pretopos to be a cocomplete LCC pretopos; it is easy to see that a -pretopos is also complete.)
I have been writing all this down on my web page here, including proofs of my assertions in 2 above (I haven’t tackled -types yet). Some of it might be a bit clunky. But the basic upshot is that the free small-colimit cocompletion of a -pretopos is also a -pretopos (and almost never a topos). It bothers me though that all this is a bit abstract; I’m having trouble picturing the nature of these constructions.
1 to 5 of 5