Add three categories of large families of sets

[ScriptRaccoon]

This PR adds three categories that are defined similarly but have very different properties. Here, $I$ is a collection that is not essentially small.

• the category Set^(I)₁ of $I$-indexed families $X$ of sets which are mostly singletons, i.e. the collection of $i \in I$ for which $X_i$ is not a singleton is essentially small
• the category Set^(I)₀ of $I$-indexed families $X$ of sets which are mostly empty, i.e. the collection of $i \in I$ for which $X_i$ is not empty is essentially small
• the product category Set^I of all $I$-indexed families of sets

These categories are similar to Vect^(I) from #365. All properties have been decided.

The motivation was to contribute to this milestone and to add an example of a cartesian closed category without a generating collection. In fact, Set^(I)₁ is such an example, while Set^(I)₀ is at least a locally cartesian closed category without a generating collection; this combination was also missing before.

The product category Set^I provides the first example of a category in the database that is cartesian closed and not locally essentially small, but it satisfies lots of other new combinations as well (44). For example, it is an elementary topos without a generating collection.

In total, 57 new combinations are witnessed by the three categories, and the number of missing combinations has decreased from 467 to 410.

Found 57 unique witnessed combinations by the supplied structures (Set_family, Set_family_mostly_0, Set_family_mostly_1):

Directly witnessed:
- elementary topos ∧ ¬accessible
- quasitopos ∧ ¬accessible
- subobject classifier ∧ ¬accessible
- cartesian closed ∧ ¬concretizable
- elementary topos ∧ ¬concretizable
- quasitopos ∧ ¬concretizable
- regular subobject classifier ∧ ¬concretizable
- subobject classifier ∧ ¬concretizable
- elementary topos ∧ ¬extremal generating collection
- pretopos ∧ ¬extremal generating collection
- quasitopos ∧ ¬extremal generating collection
- subobject classifier ∧ ¬extremal generating collection
- cartesian closed ∧ ¬generating collection
- elementary topos ∧ ¬generating collection
- locally cartesian closed ∧ ¬generating collection
- pretopos ∧ ¬generating collection
- quasitopos ∧ ¬generating collection
- regular subobject classifier ∧ ¬generating collection
- subobject classifier ∧ ¬generating collection
- cartesian closed ∧ ¬locally essentially small
- elementary topos ∧ ¬locally essentially small
- quasitopos ∧ ¬locally essentially small
- regular subobject classifier ∧ ¬locally essentially small
- subobject classifier ∧ ¬locally essentially small
- cartesian closed ∧ ¬well-copowered
- elementary topos ∧ ¬well-copowered
- quasitopos ∧ ¬well-copowered
- regular subobject classifier ∧ ¬well-copowered
- subobject classifier ∧ ¬well-copowered
- elementary topos ∧ ¬well-powered
- quasitopos ∧ ¬well-powered
- subobject classifier ∧ ¬well-powered
- elementary topos ∧ ¬ℵ₁-accessible
- quasitopos ∧ ¬ℵ₁-accessible
- complete ∧ ¬natural numbers object
- countable powers ∧ ¬natural numbers object
- countable products ∧ ¬natural numbers object
- powers ∧ ¬natural numbers object
- products ∧ ¬natural numbers object
- ℵ₂-small powers ∧ ¬natural numbers object
- ℵ₂-small products ∧ ¬natural numbers object

Dually witnessed:
- quotient object classifier ∧ ¬coaccessible
- cocartesian coclosed ∧ ¬concretizable
- regular quotient object classifier ∧ ¬concretizable
- quotient object classifier ∧ ¬concretizable
- quotient object classifier ∧ ¬extremal cogenerating collection
- cocartesian coclosed ∧ ¬cogenerating collection
- locally cocartesian coclosed ∧ ¬cogenerating collection
- regular quotient object classifier ∧ ¬cogenerating collection
- quotient object classifier ∧ ¬cogenerating collection
- cocartesian coclosed ∧ ¬locally essentially small
- regular quotient object classifier ∧ ¬locally essentially small
- quotient object classifier ∧ ¬locally essentially small
- cocartesian coclosed ∧ ¬well-powered
- regular quotient object classifier ∧ ¬well-powered
- quotient object classifier ∧ ¬well-powered
- quotient object classifier ∧ ¬well-copowered

It is a great surprise to me that Set^(I)₁ is the first example of a category in the database that is complete (or even has powers) but does not have a natural numbers object.

Moreover, a result has been strengthened, stating that a cartesian closed category with an initial object has a strict initial object. In fact, this already holds in a locally cartesian closed category.

Finally, the category [Set_disc, Ab] has been renamed and generalized to Ab^I. Its ID changed from Set_disc_Ab to Ab_family. As for the category Vect^(I), its ID Vect_family has been changed to Vect_family_mostly_0 to differentiate it from Vect^I (which is not in the database yet, but we have the variants Set^I and Ab^I already).