Add various categories with subobject classifiers

[ScriptRaccoon]

TODO. decide the remaining properties of the category of connected sequences.

---

This PR adds various examples of categories with subobject classifiers and finite limits*, while not satisfying some other properties. The goal is to reduce the number of missing combinations, cf. this milestone. The categories are listed below.

*This is currently included in the definition of a subobject classifier, but might change later (#370).

The category of finite-or-empty pairs of sets

This is a rather random category, the full subcategory of Set × Set consisting of pairs (A,B) where A is empty or B is finite. It serves as an example of a category with a subobject classifier, but without binary coproducts. All properties have been decided.

The category of directed graphs with finite components

This is the full subcategory of DiGraph consisting of coproducts of finite directed graphs. It is an example of a category with a subobject classifier, but without coequalizers. All properties have been decided.

The category of sequences of sets

This is the functor category [(N,≤),Set]. It shares exactly the same properties (currently) as the Sierpinski topos Mor(Set). In particular, all properties have been decided, and no new combinations are witnessed. I have added this category to prepare for the next example.

The category of connected sequences of sets

We also add the full subcategory of [(N,≤),Set] consisting of connected sequences $X_0 \to X_1 \to \cdots$, meaning that $colim_n X_n$ is a singleton. It has been suggested by Jonas Frey at mathoverflow and provides an example of a category with a subobject classifier, but without initial object (and no binary copowers, hence also no binary coproducts, just like the first category in the list).

TODO. decide all of its properties; for example, it should be be finitely accessible

New combinations

In total, the categories satisfy 45 new combinations. The number of missing combinations goes down from 399 to 354.

TODO. update this number when finished

Found 45 unique witnessed combinations by the supplied structures (SetxSet_0_fin, DiGraph_fc, SeqSet_conn):

Directly witnessed:
- subobject classifier ∧ ¬Barr-coexact
- subobject classifier ∧ ¬Barr-exact
- subobject classifier ∧ ¬co-Malcev
- regular subobject classifier ∧ ¬coequalizers
- subobject classifier ∧ ¬coequalizers
- subobject classifier ∧ ¬coregular
- subobject classifier ∧ ¬effective congruences
- subobject classifier ∧ ¬finitely cocomplete
- subobject classifier ∧ ¬pushouts
- regular subobject classifier ∧ ¬quotients of congruences
- subobject classifier ∧ ¬quotients of congruences
- ℵ₁-accessible ∧ ¬quotients of congruences
- ℵ₁-filtered colimits ∧ ¬quotients of congruences
- regular subobject classifier ∧ ¬reflexive coequalizers
- subobject classifier ∧ ¬reflexive coequalizers
- subobject classifier ∧ ¬regular
- subobject classifier ∧ ¬binary copowers
- subobject classifier ∧ ¬binary coproducts
- subobject classifier ∧ ¬disjoint finite coproducts
- subobject classifier ∧ ¬finite copowers
- subobject classifier ∧ ¬finite coproducts
- subobject classifier ∧ ¬initial object
- subobject classifier ∧ ¬multi-initial object

Dually witnessed:
- quotient object classifier ∧ ¬Barr-exact
- quotient object classifier ∧ ¬Barr-coexact
- quotient object classifier ∧ ¬Malcev
- regular quotient object classifier ∧ ¬equalizers
- quotient object classifier ∧ ¬equalizers
- quotient object classifier ∧ ¬regular
- quotient object classifier ∧ ¬effective cocongruences
- quotient object classifier ∧ ¬finitely complete
- quotient object classifier ∧ ¬pullbacks
- regular quotient object classifier ∧ ¬coquotients of cocongruences
- quotient object classifier ∧ ¬coquotients of cocongruences
- ℵ₁-cofiltered limits ∧ ¬coquotients of cocongruences
- regular quotient object classifier ∧ ¬coreflexive equalizers
- quotient object classifier ∧ ¬coreflexive equalizers
- quotient object classifier ∧ ¬coregular
- quotient object classifier ∧ ¬binary powers
- quotient object classifier ∧ ¬binary products
- quotient object classifier ∧ ¬disjoint finite products
- quotient object classifier ∧ ¬finite powers
- quotient object classifier ∧ ¬finite products
- quotient object classifier ∧ ¬terminal object
- quotient object classifier ∧ ¬multi-terminal object