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 C is a complete and cocomplete Π-pretopos, then we have an evident functor Δ:Set→C and I believe
(Note: it may be shown that C↓Δ, for C an ∞-lextensive category, is the free small-coproduct completion of C.) Furthermore, if Eex denotes the ex/lex completion, then
One import of this is that the free small-colimit completion Colim(C), for C a complete and cocomplete Π-pretopos, is equivalent to (C↓Δ)ex, which by the above is also a complete and cocomplete Π-pretopos.
Furthermore, I conjecture that the above stability theorems carry over to Π-W-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 G:E→E is a pullback-preserving comonad, then the underlying functor U:CoalgG→E preserves and reflects colimits and pullbacks, and this means that the pretopos axioms hold on CoalgG if they hold on E. 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 E is locally cartesian closed, then so is CoalgG. (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 W-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