document redundancy script

Author: ScriptRaccoon

CONTRIBUTING.md

@@ -110,7 +110,7 @@ When contributing new data (categories, functors, properties, implications), ple
 
 - **Reduce Unknowns**: Try to reduce the number of unknown properties of categories, in particular when adding a new category. Use the category detail page to see its unknown properties. Use the [page with missing data](https://catdat.app/missing) to identify categories with unknown properties. The same remarks apply to functors.
 
-- **Atomic Properties**: Only assign properties to a category or functor that cannot be deduced from other properties (satisfied or not). For example, if a category is complete, add the property "complete", but do not add "terminal object". The application infers this property automatically.
+- **Avoid redundant assignments**: Only assign properties (satisfied or not) to a category or functor if they cannot be deduced from other assignments. For example, if a category is complete, record that it is complete, but do not also record that it has a terminal object; the application infers this automatically. Redundant assignments can be identified using the redundancy script described below.
 
 - **No dual categories**: Instead of adding the dual of a category already in the database, consider adding properties to the original category (use the corresponding dual properties).
 
@@ -138,6 +138,26 @@ When contributing new data (categories, functors, properties, implications), ple
 
 - **New Combinations**: Add new categories that satisfy combinations of satisfied properties and unsatisfied properties and not yet in the database. For example, you may add a category that is abelian but neither cocomplete nor essentially small (if it is not already present). The [page with missing data](https://catdat.app/missing) lists consistent combinations of the form $p \land \neg q$ that are not yet witnessed by a category in the database. The same remarks apply to functors.
 
+### Redundancy Script
+
+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.
+
 ### Keep Pull Requests Focused
 
 Please keep each pull request limited in scope. Large pull requests are harder to review, more likely to conflict with ongoing changes on the main branch, and more difficult to merge cleanly.

DATABASE.md

@@ -33,6 +33,7 @@ Further tables are:
 - `special_morphisms`
 - `related_category_properties`
 - `category_comments`
+- `category_property_comments`
 - `lemmas` (a flexible variant of implications)
 
 For functors there are similar tables, such as:
@@ -64,6 +65,10 @@ Use `pnpm db:update` to run all the commands in sequence: `pnpm db:seed`,`pnpm d
 
 Use `pnpm db:watch` to run this command automatically every time a file in the subfolder [/databases/catdat/data](/databases/catdat/data) changes. This is useful in particular during development.
 
+## Redundancies
+
+There is another script that intentionally does not run with each update: `pnpm db:redundancies` checks for redundant assignments of properties ot categories.
+
 ## Diagram
 
 This is the database schema as of 24.04.2026; changes may occur.