Combine special objects and special morphisms with property assignments

[ScriptRaccoon]

The concepts of special objects and special morphisms of categories is very similar to the concept of properties of categories. There is clearly a connection between the two, but the code does not currently make this explicit and instead suffers from code duplication.

Here are some (unfinished) thoughts.

1. When a category has the property that an initial object exists, it should have an entry for this special object. Currently, there is no connection between the two.
2. The descriptions of coproducts that only apply in the finite case are clumsy (for example for FinSet); they simply start with a [finite case] note. Instead, they should be connected to the property of having finite coproducts.
3. When a category has a description of, say, its regular monomorphisms, this requires a proof, just as a property assignment requires a proof. Currently, however, these are represented by two completely different tables and treated as two completely different concepts in the code.
4. On the other hand, information about what regular monomorphisms look like is a text-based value, whereas information about whether a category is, say, abelian is a boolean value.
5. Many proofs of properties of categories are intertwined with proofs of descriptions of their special morphisms and special objects. It is unclear whether both directions are allowed and whether circular reasoning can occur without being noticed.
6. The table special_morphism_rules (introduced in Automatic deduction of special morphisms #285) has a very similar purpose as the table implications. It automaticaly assigns descriptions of special morphisms when the category has a certain property.
7. So what exactly is a "special morphism assignment"? Can we use the existing morphisms structure type to make this precise?
8. We need to find an approach that is not specific to categories. In any case, it would be useful to think about this more generally: perhaps we also want to describe special things associated with functors, special morphisms in monoidal categories, etc.