Add quasitopos property

[dschepler]

Adds properties: quasitopos, Grothendieck quasitopos
As a prototypical example of the latter, adds the category of separated presheaves on a topological space

[ScriptRaccoon]

Can we perhaps also add (directly in this PR) a simple but interesting example of a quasi-topos which is not a topos? Currently the examples are all thin, thus not interesting.

https://catdat.app/category-search/results?satisfied=finitely_complete%7Efinitely_cocomplete%7Elocally_cartesian_closed%7Eregular_subobject_classifier&unsatisfied=elementary_topos%7Ethin

The nlab page mentions some examples.

[ScriptRaccoon]

I think https://ncatlab.org/nlab/show/subsequential+space would be a nice example.

[ScriptRaccoon]

Thank you for the PR! I made some minor comments. I haven't checked out the code yet in my editor, I will do that tomorrow.

---

Related issue: #18

[dschepler]

Actually, could you check Johnstone C2.2.13 for the exact statement, and if it matches what's on the nLab page, could you check whether the definition of "generating set" he uses matches the one we use? If so, then I'd think the category of pseudotopological spaces would be a counterexample to the first statement: it's certainly a locally small quasitopos; it's cocomplete (for arbitrary coproducts, take the disjoint union and set the convergent filters to be exactly the ones containing an image of a convergent filter in one of the components); and it has a generating set (in fact it's even well-pointed). I suspect that the correct statement of the first one would have to replace "generating set" with "small dense subcategory".

If that's the case, then we don't currently have all the component properties of either formulation. Though I guess I could approximate it with a combination of the two, "Grothendieck quasitopos <-> quasitopos + locally small + locally presentable". EDIT: Actually I guess locally presentable -> locally essentially small so that becomes Grothendieck quasitopos <-> quasitopos + locally presentable.

[ScriptRaccoon]

I don't understand the context of your comment. Are you reviewing something which is already in the PR? Is there something wrong? What do you mean with "first statement" in "If so, then I'd think the category of pseudotopological spaces would be a counterexample to the first statement"?

Are you thinking of adding the result C2.2.13 to the implications?

Here is the definition (urgh...)

[dschepler]

The context was that I was considering adding "Grothendieck quasitopos" property to the PR, and then the example of SepPsh(X) as an example of a Grothendieck quasitopos which is not an elementary topos (under the assumption that the topology on X is not totally ordered under inclusion). So I wanted to evaluate what would be a correct equivalent condition, hopefully using existing properties.

The "first statement" was referring to the restatement of this theorem on the nLab quasitopos page, which corresponds to the equivalence (ii) <=> (iii) in Johnstone's theorem.

So, it does look like Johnstone's definition of "generating set" is different from ours (which he calls "separating set"). Johnstone's version certainly seems related to being able to express objects as colimits of generating objects, though I'm not sure of the exact relation off the top of my head.

[ScriptRaccoon]

I understand. But I won't be able to help with that, I am afraid. Maybe it's also necessary to edit the nLab article or reach out to the authors since it "misquotes" (because of Johnstone's weird terminology) the theorem.