Add "pretopos" and related properties

[dschepler]

For topos theory aficionados, it might be interesting to add the "pretopos" property, which would also prompt adding some of the component properties. For the latter, I haven't done a thorough investigation of what might already be there: regular (having mono-epi factorizations which are stable under pullbacks); (Barr-)exact (regular and having "strict" quotients of all internal equivalence relations); extensive (though I do remember seeing the related property lextensive).

That might also prompt adding a category example of the category of compact Hausdorff topological spaces, which is an example of pretopos + cartesian closed + ~ subobject classifier (+ the forgetful functor to Set is monadic).

I realize that might be a lot to add, and classify especially some of the component properties for existing categories - so if you want, I could maybe take a deeper look at what would be involved in creating a PR for this myself, though it might be a little while before I can find the time for that.

I don't know that we'd need to add all the variants at the ncatlab page, such as W-pretopos, $\Pi$-pretopos, etc. - at least not in this go around.

[dschepler]

It actually turns out that the category of compact Hausdorff topological spaces isn't cartesian closed. Even though exponentials of such spaces exist in Top, those exponentials are not necessarily compact themselves. So, that remains just an example of pretopos + ~ cartesian closed + ~ subobject classifier (+ cogenerator incidentally: [0,1] works essentially by Urysohn's lemma).

On the other hand, the category of countable sets is an example of pretopos + subobject classifier + ~ cartesian closed.

I don't know of any examples of pretopos + cartesian closed + ~ subobject classifier, other than perhaps the example of formal expressions in a type theory with function types but no type of all propositions, which probably is too specialized an example to include in the database.

[dschepler]

I also don't know whether it might be worthwhile to separate out "has quotients of internal equivalence relations" from Barr-exact. Here, I have in mind an example I saw on MSE where the category of undirected graphs is regular, extensive, and has quotients of internal equivalence relations, but those quotients are not necessarily strict, so that fails to be a pretopos just on that one point. (On the other hand, the category of directed graphs is, of course, a Grothendieck topos.)