Add effective topos #353

An idea I've been toying around with is to see what it would take to add the effective topos to the database: https://ncatlab.org/nlab/show/effective+topos

For example, I think this is an example of an elementary topos with natural numbers object which does not have countable copowers (and in fact the natural numbers object is not a countable copower of the terminal object).

I'm not sure how well I'd be able to assign other properties, though. I think I've just barely gotten to the point where I can grasp the basic definitions of what an object is and what a morphism is, and I can start to reason about the category.

(Anyway, my immediate plans would be to finish off the quasitopos project by adding a property for "has effective regular congruences" - the grouping is "has effective (regular congruences)" rather than "has (effective and regular) congruences". Then add the Grothendieck quasitopos property, and then maybe add the category SepPsh(X) for X a topological space. And then possibly a few of the other examples we've discussed, such as "category of sets equipped with a binary relation", "category of subsequential spaces", "category of pseudotopological spaces" (that one I think would be an example of a complete and cocomplete quasitopos which is not a Grothendieck quasitopos because it doesn't have a small extremal generating set), "category of simple graphs".)