Add the category of countable sets

[ScriptRaccoon]

This adds the category of countable sets to the database. This fits nicely to the numerous "countable" properties in the database (such as "countably distributive" and having "countable products"), and the category has appeared in the proof that Man is not $\aleph_1$-accessible anyway. This proof could now be refactored.

All properties have been decided. While doing so, it became clear that #22 should become a priority. Most of these "works as for the category of sets" arguments should be automated somehow.

At some point we can maybe also add the property "countably extensive" since the category of countable sets is a prime example for this. And then we can also remove the manual proof that it is countably distributive, since of course "extensive => distributive" can be adjusted to "countably extensive => countably distributive".

I assume that the category of countable sets is $\aleph_2$-accessible, but currently this property is not in the database. For now, it is only registered as accessible because of essentially small + Cauchy complete => accessible.