Add Redundancy Tests

[ScriptRaccoon]

This PR resolves #153 by adding a script pnpm db:redundancies that checks for redundant assignments of properties.

This PR also removes all 39 redundant assignments of unsatisfied properties. Some proofs generated by CatDat are quite clever, some are easy. It also removes 25 redundant assignments of satisfied properties.

For satisfied properties, I did not remove all redundant assignments, because in some cases, there were good reasons to keep them (see below). Accordingly, I also added an option to let the script skip these.

Documentation in Contribution Guidelines

"As noted above, avoid redundant property assignments to a category. To detect redundancies, run pnpm db:redundancies.

The script reports at most one redundant assignment per category for each of satisfied and unsatisfied properties, even if multiple exist. After removing an assignment, run the script again to ensure that all remaining redundancies are handled.

Removing redundant assignments is not required, but it is recommended, especially for all unsatisfied properties. For satisfied properties, removal depends on context: keep them if the proof is meaningful, otherwise consider removing them if it is purely technical or uninformative.

In particular, it often makes sense to keep a redundant assignment of a satisfied property in the following cases:

• The proof for the property is straight forward anyway (e.g. showing that a category is pointed).
• The proof provides useful insight.
• The proof constructs objects (especially limits or colimits) that are used later.
• Removing the assignment would lead to an overly complex deduction generated by CatDat.
• The proof establishes an intermediate result that is used as an assumption in a later argument.

For example, you may first prove that a category has zero morphisms, and then prove that it is normal. Although the database contains the implication "normal => zero morphisms", in practice the latter is used as a prerequisite. Similarly, when proving that a category is extensive, it is often clearer to first show that finite coproducts exist, rather than relying on the implication "extensive => finite coproducts". Also, an explicit description of finite coproducts is useful for deciding other properties involving coproducts.

Every redundant assignment of a satisfied property that is intentionally kept must be explicitly marked to skip the redundancy check. See N.sql for an example."

How to keep redundant assignments

--- File: N.sql
 
-- properties that should be ignored by the redundancy check script
UPDATE category_property_assignments
SET check_redundancy = FALSE
WHERE category_id = 'N'
AND property_id IN ('thin', 'finitely cocomplete');

Example Output

--- Check redundant category property assignments ---
🟠 Redundant satisfied property for Man: "well-powered" is implied by others.
🟠 Redundant satisfied property for TorsAb: "cocomplete" is implied by others.
🟠 Redundant satisfied property for TorsFreeAb: "complete" is implied by others.
🟠 Redundant satisfied property for BN: "pullbacks" is implied by others.
🟠 Redundant satisfied property for BOn: "pullbacks" is implied by others.
🟠 Redundant satisfied property for N_oo: "coproducts" is implied by others.
🟠 Redundant satisfied property for Z_div: "products" is implied by others.
Found 7 redundant assignments

[dschepler]

Looks good to me.

[ScriptRaccoon]

Thank you for having a look!