Dualize all properties #364

All properties in the database should eventually have a dual. Only then does the deduction system work fully*. Moreover, although a property's dual may be less common, it corresponds to a common property of the dual category and is therefore interesting in its own right.

From now on, every new property should have a dual. Any PR adding a property $P$ must also add $P^{\mathrm{op}}$.

The following properties currently do not have a dual. The list of PRs will be updated.

Query:

SELECT id, type FROM properties WHERE dual_property_id IS NULL;

Maybe "representable functors" cannot be dualized since their target is fixed. In any case, the focus should be on categories. (EDIT: I have decided that representability does not need to have a dual.)

For each added dual property, it should be decided for as many categories as possible whether they satisfy it or not. In many cases, this is already done via the deduction system, which automatically dualizes implications. For example, when adding "co-natural numbers object" and "parametrized co-natural numbers object", the first property is automatically decided for all categories in the database, while the second only remains to be decided for the categories of (commutative) algebras and (commutative) rings.

A typical situation is the following. We have properties with duals $P$ and $Q$, and an implication $P \Rightarrow Q$. This implication is automatically dualized. We add a new property $R$, which does not yet have a dual, and add it as a conclusion of the implication: $P \Rightarrow Q$ and $R$. But now the implication is no longer dualized, so we lose $P^{\mathrm{op}} \Rightarrow Q^{\mathrm{op}}$. We need to make this a separate implication: $P \Rightarrow R$. This has been forgotten a couple of times (for example, when $\aleph_1$-accessible was added).

Another issue appears in walking_coreflexive_pair.yaml, where the proof of the negation of multi-complete has to be done manually just because locally multi-presentable has not yet been dualized. (EDIT: done)

There is also a comment for the implication finite_filtered_colimits that needs to be addressed when we add "finitely coaccessible". (EDIT: done)

When adding the dual of "generalized variety", take care of the comment for groupoids_are_finitely_accessible. (EDIT: no longer relevant)