Add Functors to CatDat

.vscode/settings.json

@@ -19,6 +19,8 @@
 	],
 	"cSpell.words": [
 		"abelian",
+		"abelianization",
+		"abelianize",
 		"Adamek",
 		"algébriques",
 		"anneaux",
@@ -44,12 +46,15 @@
 		"coequalizer",
 		"coequalizers",
 		"cofiltered",
+		"cofinitary",
 		"cogenerates",
 		"cogenerating",
 		"cogenerator",
 		"cokernel",
 		"colimit",
 		"colimits",
+		"comonad",
+		"comonadic",
 		"conormal",
 		"coprime",
 		"coproduct",
@@ -141,6 +146,7 @@
 		"rng",
 		"rngs",
 		"Rosicky",
+		"saft",
 		"Schapira",
 		"semisimple",
 		"setoid",

CONTRIBUTING.md

@@ -67,39 +67,39 @@ If the local database is broken, just delete the `local.db` file and recreate it
 
 ### Guidelines for Adding New Data
 
-When contributing new data (categories, properties, implications), please follow these guidelines:
+When contributing new data (categories, functors, properties, implications), please follow these guidelines:
 
 - **Consistency**: Stick to the format indicated by the existing data. This is enforced by the database definition.
 
-- **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.
+- **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 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.
+- **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.
 
 - **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).
 
 - **No equivalent categories**: Do not add categories that are equivalent or even isomorphic to categories already in the database. If the equivalence is non-trivial, mention it in the description of the original category. Some exceptions are allowed, since certain properties (such as being skeletal) are not invariant under equivalence.
 
 - **Special Objects and Morphisms**: For each new category, try to specify its special objects (terminal object, initial object, etc.) in the corresponding table. Also try to specify its special morphisms (isomorphisms, monomorphisms, epimorphisms).
 
-- **Proofs for New Properties**: For every new property, for each existing category, try to find a proof for whether it has this property or not, in case this has not already been deduced automatically. Use the property detail page to check unknown categories.
+- **Proofs for New Properties**: For every new property, for each existing category or functor, try to find a proof for whether it has this property or not, in case this has not already been deduced automatically. Use the property detail page to check unknown categories.
 
-- **Assign Properties to Core Categories**: For all new properties, you must assign them to the "core categories" (currently: $\mathbf{Set}$, $\mathbf{Top}$, $\mathbf{Ab}$), specifying whether they are satisfied or not. This decision should also be recorded in the JSON files located in [/scripts/expected-data](/scripts/expected-data/).
+- **Assign Properties to Core Categories**: For all new properties of categories, you must assign them to the "core categories" (currently: $\mathbf{Set}$, $\mathbf{Top}$, $\mathbf{Ab}$), specifying whether they are satisfied or not. This decision should also be recorded in the JSON files located in [/scripts/expected-data](/scripts/expected-data/).
 
-- **Counterexamples**: Ensure that at least one category does not satisfy any new property that is added. If no existing category fits, add a new category that does not have the new property.
+- **Counterexamples**: Ensure that at least one category does not satisfy any new property of categories that is added. If no existing category fits, add a new category that does not have the new property. The same remarks apply to properties of functors.
 
-- **Positive Properties**: Do not add negated properties to the database. For example, do not add "large" as the negation of "small". Instead, add "small" to the list of unsatisfied properties for a category. As a rule of thumb, every registered property should be satisfied at least by the trivial category.
+- **Positive Properties**: Do not add negated properties to the database. For example, do not add "large" as the negation of "small". Instead, add "small" to the list of unsatisfied properties for a category. As a rule of thumb, every registered property of categories should be satisfied at least by the trivial category. Similarly, every property of functors should be satisfied at least by the identity functor.
 
 - **Proofs for Claims**: Provide proofs for all new claims (satisfied properties, unsatisfied properties, implications, special morphisms). (We are currently working on filling in the existing ones.)
 
 - **Atomic Implications**: Do not add implications that can be deduced from others. For example, do not add "complete => finite products" since it can be deduced from "complete => finitely complete" and "finitely complete => finite products". These are deduced automatically.
 
-- **No dual implications**: Implications are dualized automatically when applicable. For this reason, adding "finitely cocomplete => pushouts" is not necessary when "finitely complete => pullbacks" has already been added.
+- **No dual implications**: Implications are dualized automatically when applicable. For this reason, adding the category implication "finitely cocomplete => pushouts" is not necessary when "finitely complete => pullbacks" has already been added. Similarly, the functor implication "comonadic => left adjoint" is automatically dualized from "monadic => right adjoint".
 
-- **Relevant implications**: When adding a new property, include implications involving this property and existing properties. For example, when adding "countable products", also add "countable products => finite products". Refactor existing implications if necessary. Ensure that for most categories, it will be inferred if the property holds or not.
+- **Relevant implications**: When adding a new property, include implications involving this property and existing properties. For example, when adding the property of categories of having "countable products", also add the implication "countable products => finite products". Refactor existing implications if necessary. Ensure that for most categories and functors, it will be inferred if the property holds or not.
 
 - **Simplify Implications**: When adding a new implication, check if it simplifies existing implications and if it deduces some previously non-deduced properties for categories.
 
-- **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.
+- **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.
 
 ## Option 3: Create an Issue
 

DATABASE.md

@@ -58,6 +58,6 @@ Use `pnpm db:watch` to run this command automatically every time a file in the s
 
 ## Diagram
 
-This is the database schema as of 27.03.2016; changes may occur.
+This is the database schema as of 31.03.2016; changes may occur.
 
-<img alt="database diagram" src="https://github.com/user-attachments/assets/9f482625-8c19-4050-a72c-109399a832f0" />
+<img alt="database diagram" src="https://github.com/user-attachments/assets/71c5a6f6-2747-4692-8518-d562dbd51a91" />

README.md

@@ -7,19 +7,20 @@
 
 ## [**https://catdat.app**](https://catdat.app)
 
-_CatDat_ provides a growing collection of categories, each with detailed descriptions
+_CatDat_ provides a growing collection of categories and functors, each with detailed descriptions
 and properties. Built by and for those who love [category theory](https://en.wikipedia.org/wiki/Category_theory).
 
 [Watch the YouTube video](https://youtu.be/dQXbPxk__qA)
 
 ## Features
 
-- **Category Detail Pages**: Explore a category’s definition, its satisfied and unsatisfied properties, and related categories.
-- **Property Detail Pages**: Explore the definition of a property and view categories that satisfy it and those that don't.
+- **Category Detail Pages**: Explore a category's definition, its satisfied and unsatisfied properties, and related categories.
+- **Functor Detail Pages**: Explore a functors's definition along with its satisfied and unsatisfied properties.
+- **Property Detail Pages**: Explore the definition of a property and view categories or functors that satisfy it and those that don't.
 - **Reasons and References**: Each property and implication includes a reason or reference, forming a data-driven knowledge base for category theory.
-- **Deduction System**: Automatically infers properties from existing ones using a database of implications.
+- **Deduction System**: Automatically infers properties from existing ones using a database of implications, both for categories and functors.
 - **Automatic Dualization**: Automatically dualizes implications and property assignments.
-- **Searchable Database**: Find categories based on satisfied properties and unsatisfied properties.
+- **Searchable Database**: Find categories and functors based on satisfied properties and unsatisfied properties.
 - **Comparison Feature**: Compare multiple categories to identify their differences and similarities.
 - **Customizable Display**: Light/dark mode and optional display of deduced properties.
 - **Intuitive User Interface**: Usable on both mobile and desktop.

database/data/000_setup/001_clear.sql

@@ -21,6 +21,17 @@ DELETE FROM tags;
 
 DELETE FROM related_properties;
 DELETE FROM properties;
+
+DELETE FROM functor_property_assignments;
+DELETE FROM functor_properties;
+DELETE FROM functors;
+
 DELETE FROM relations;
 
+DELETE FROM functor_implication_assumptions;
+DELETE FROM functor_implication_conclusions;
+DELETE FROM functor_implication_source_assumptions;
+DELETE FROM functor_implication_target_assumptions;
+DELETE FROM functor_implications;
+
 PRAGMA foreign_keys = ON;