diff --git a/.vscode/settings.json b/.vscode/settings.json
index a4a0f50e..6c7f4745 100644
--- a/.vscode/settings.json
+++ b/.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",
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 812c43dc..4b074754 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -67,13 +67,13 @@ 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).
@@ -81,25 +81,25 @@ When contributing new data (categories, properties, implications), please follow
- **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
diff --git a/DATABASE.md b/DATABASE.md
index d04cd6dc..c37fbecf 100644
--- a/DATABASE.md
+++ b/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.
-
+
diff --git a/README.md b/README.md
index 44aa7009..a565b17c 100644
--- a/README.md
+++ b/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.
diff --git a/database/data/000_setup/001_clear.sql b/database/data/000_setup/001_clear.sql
index 3549f8d1..6f8a85c8 100644
--- a/database/data/000_setup/001_clear.sql
+++ b/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;
\ No newline at end of file
diff --git a/database/data/008_functors/001_functor-properties.sql b/database/data/008_functors/001_functor-properties.sql
new file mode 100644
index 00000000..c36f70b1
--- /dev/null
+++ b/database/data/008_functors/001_functor-properties.sql
@@ -0,0 +1,232 @@
+INSERT INTO functor_properties (
+ id,
+ relation,
+ description,
+ nlab_link,
+ invariant_under_equivalences,
+ dual_property_id
+)
+VALUES
+ (
+ 'faithful',
+ 'is',
+ 'A functor is faithful when it is injective on Hom-sets: If $F(f)=F(g)$, then $f=g$.',
+ 'https://ncatlab.org/nlab/show/faithful+functor',
+ TRUE,
+ 'faithful'
+ ),
+ (
+ 'full',
+ 'is',
+ 'A functor is full when it is surjective on Hom-sets: Every morphism $F(A) \to F(B)$ is induced by a morphism $A \to B$.',
+ 'https://ncatlab.org/nlab/show/full+functor',
+ TRUE,
+ 'full'
+ ),
+ (
+ 'essentially surjective',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is essentially surjective when every object $Y \in \mathcal{D}$ is isomorphic to $F(X)$ for some $X \in \mathcal{C}$.',
+ 'https://ncatlab.org/nlab/show/essentially+surjective+functor',
+ TRUE,
+ 'essentially surjective'
+ ),
+ (
+ 'equivalence',
+ 'is an',
+ 'A functor is an equivalence if it has a pseudo-inverse functor.',
+ 'https://ncatlab.org/nlab/show/equivalence+of+categories',
+ TRUE,
+ 'equivalence'
+ ),
+ (
+ 'continuous',
+ 'is',
+ 'A functor is continuous when it preserves all small limits.',
+ 'https://ncatlab.org/nlab/show/continuous+functor',
+ TRUE,
+ 'cocontinuous'
+ ),
+ (
+ 'cocontinuous',
+ 'is',
+ 'A functor is cocontinuous when it preserves all small colimits.',
+ 'https://ncatlab.org/nlab/show/cocontinuous+functor',
+ TRUE,
+ 'continuous'
+ ),
+ -- Here is why we do not call this property "preserves products":
+ -- Either we name the property "preserves products" and choose the
+ -- empty relation '' (instead of 'is'). But then negations will not be
+ -- formatted properly ("does not preserves products").
+ -- Or we name property "products" and choose the relation 'preserves'.
+ -- But then we will never be able to add the properties of "reflecting products",
+ -- "creating products", etc.
+ (
+ 'product-preserving',
+ 'is',
+ 'A functor $F$ preserves products when for every family of objects $(A_i)$ in the source whose product $\prod_i A_i$ exists, also the product $\prod_i F(A_i)$ exists in the target and such that the canonical morphism $F(\prod_i A_i) \to \prod_i F(A_i)$ is an isomorphism.',
+ NULL,
+ TRUE,
+ 'coproduct-preserving'
+ ),
+ (
+ 'coproduct-preserving',
+ 'is',
+ 'A functor $F$ preserves coproducts when for every family of objects $(A_i)$ in the source whose coproduct $\prod_i A_i$ exists, also the coproduct $\coprod_i F(A_i)$ exists in the target and such that the canonical morphism $\coprod_i F(A_i) \to F(\coprod_i A_i)$ is an isomorphism.',
+ NULL,
+ TRUE,
+ 'product-preserving'
+ ),
+ (
+ 'finite-product-preserving',
+ 'is',
+ 'A functor $F$ preserves finite products when for every finite family of objects $(A_i)$ in the source whose product $\prod_i A_i$ exists, also the product $\prod_i F(A_i)$ exists in the target and such that the canonical morphism $F(\prod_i A_i) \to \prod_i F(A_i)$ is an isomorphism.',
+ NULL,
+ TRUE,
+ 'finite-coproduct-preserving'
+ ),
+ (
+ 'finite-coproduct-preserving',
+ 'is',
+ 'A functor $F$ preserves finite coproducts when for every family of objects $(A_i)$ in the source whose coproduct $\prod_i A_i$ exists, also the coproduct $\coprod_i F(A_i)$ exists in the target and such that the canonical morphism $\coprod_i F(A_i) \to F(\coprod_i A_i)$ is an isomorphism.',
+ NULL,
+ TRUE,
+ 'finite-product-preserving'
+ ),
+ (
+ 'terminal-object-preserving',
+ 'is',
+ 'A functor $F$ preserves terminal objects when it maps every terminal object to a terminal object. It is not assumed that the source category has a terminal object.',
+ NULL,
+ TRUE,
+ 'initial-object-preserving'
+ ),
+ (
+ 'initial-object-preserving',
+ 'is',
+ 'A functor $F$ preserves initial objects when it maps every initial object to an initial object. It is not assumed that the source category has a initial object.',
+ NULL,
+ TRUE,
+ 'terminal-object-preserving'
+ ),
+ (
+ 'equalizer-preserving',
+ 'is',
+ 'A functor $F$ preserves equalizers when for every parallel pair of morphisms $f,g : A \to B$ whose equalizer $i : E \to A$ exists, also $F(i) : F(E) \to F(A)$ is an equalizer of $F(f),F(g) : F(A) \to F(B)$.',
+ NULL,
+ TRUE,
+ 'coequalizer-preserving'
+ ),
+ (
+ 'coequalizer-preserving',
+ 'is',
+ 'A functor $F$ preserves coequalizers when for every parallel pair of morphisms $f,g : A \to B$ whose coequalizer $p : B \to Q$ exists, also $F(p) : F(B) \to F(Q)$ is an coequalizer of $F(f),F(g) : F(A) \to F(B)$.',
+ NULL,
+ TRUE,
+ 'equalizer-preserving'
+ ),
+ (
+ 'left adjoint',
+ 'is a',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is a left adjoint when there is a functor $G : \mathcal{D} \to \mathcal{C}$ such that there are natural bijections $\hom(F(A),B) \cong \hom(A,G(B))$.',
+ 'https://ncatlab.org/nlab/show/left+adjoint',
+ TRUE,
+ 'right adjoint'
+ ),
+ (
+ 'right adjoint',
+ 'is a',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is a right adjoint when there is a functor $G : \mathcal{D} \to \mathcal{C}$ such that there are natural bijections $\hom(G(A),B) \cong \hom(A,F(B))$.',
+ 'https://ncatlab.org/nlab/show/right+adjoint',
+ TRUE,
+ 'left adjoint'
+ ),
+ (
+ 'monadic',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is monadic when there is a monad $T$ on $\mathcal{D}$ such that $F$ is equivalent to the forgetful functor $U^T : \mathbf{Alg}(T) \to \mathcal{D}$.',
+ 'https://ncatlab.org/nlab/show/monadic+functor',
+ TRUE,
+ 'comonadic'
+ ),
+ (
+ 'comonadic',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is comonadic when there is a comonad $T$ on $\mathcal{D}$ such that $F$ is equivalent to the forgetful functor $U^T : \mathbf{CoAlg}(T) \to \mathcal{D}$.',
+ 'https://ncatlab.org/nlab/show/comonadic+functor',
+ TRUE,
+ 'monadic'
+ ),
+ (
+ 'conservative',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is conservative when it is isomorphic-reflecting: If $f$ is a morphism in $\mathcal{C}$ such that $F(f)$ is an isomorphism, then $f$ is an isomorphism.',
+ 'https://ncatlab.org/nlab/show/conservative+functor',
+ TRUE,
+ 'conservative'
+ ),
+ (
+ 'finitary',
+ 'is',
+ 'A functor is finitary when it preserves filtered colimits.',
+ 'https://ncatlab.org/nlab/show/finitary+functor',
+ TRUE,
+ 'cofinitary'
+ ),
+ (
+ 'cofinitary',
+ 'is',
+ 'A functor is cofinitary when it preserves cofiltered limits.',
+ NULL,
+ TRUE,
+ 'finitary'
+ ),
+ (
+ 'left exact',
+ 'is',
+ 'A functor is left exact when it preserves finite limits.',
+ 'https://ncatlab.org/nlab/show/exact+functor',
+ TRUE,
+ 'right exact'
+ ),
+ (
+ 'right exact',
+ 'is',
+ 'A functor is right exact when it preserves finite colimits.',
+ 'https://ncatlab.org/nlab/show/exact+functor',
+ TRUE,
+ 'left exact'
+ ),
+ (
+ 'exact',
+ 'is',
+ 'A functor is exact when it is left exact and right exact.',
+ 'https://ncatlab.org/nlab/show/exact+functor',
+ TRUE,
+ 'exact'
+ ),
+ (
+ 'representable',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ is representable if $\mathcal{C}$ is locally small, $\mathcal{D} = \mathbf{Set}$, and there is an object $A \in \mathcal{C}$ with $F \cong \mathrm{Hom}(A,-)$.',
+ 'https://ncatlab.org/nlab/show/representable+functor',
+ TRUE,
+ NULL
+ ),
+ (
+ 'monomorphism-preserving',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ preserves monomorphisms if every monomorphism in $\mathcal{C}$ is mapped to a monomorphism in $\mathcal{D}$. This property is useful to rule out some adjunctions.',
+ 'https://ncatlab.org/nlab/show/monomorphism',
+ TRUE,
+ 'epimorphism-preserving'
+ ),
+ (
+ 'epimorphism-preserving',
+ 'is',
+ 'A functor $F : \mathcal{C} \to \mathcal{D}$ preserves epimorphisms if every epimorphism in $\mathcal{C}$ is mapped to an epimorphism in $\mathcal{D}$. This property is useful to rule out some adjunctions.',
+ 'https://ncatlab.org/nlab/show/epimorphism',
+ TRUE,
+ 'monomorphism-preserving'
+ );
diff --git a/database/data/008_functors/002_functor-implications.sql b/database/data/008_functors/002_functor-implications.sql
new file mode 100644
index 00000000..f503b864
--- /dev/null
+++ b/database/data/008_functors/002_functor-implications.sql
@@ -0,0 +1,172 @@
+INSERT INTO functor_implication_input (
+ id,
+ assumptions,
+ source_assumptions,
+ target_assumptions,
+ conclusions,
+ reason,
+ is_equivalence
+)
+VALUES
+ (
+ 'equivalence_criterion',
+ '["full", "faithful", "essentially surjective"]',
+ '[]',
+ '[]',
+ '["equivalence"]',
+ 'This is standard, see Mac Lane, Ch. IV, Theorem 4.1.',
+ TRUE
+ ),
+ (
+ 'continuous_consequences',
+ '["continuous"]',
+ '[]',
+ '[]',
+ '["product-preserving", "equalizer-preserving", "cofinitary"]',
+ 'This is trivial.',
+ FALSE
+ ),
+ (
+ 'products_consequences',
+ '["product-preserving"]',
+ '[]',
+ '[]',
+ '["finite-product-preserving"]',
+ 'This is trivial.',
+ FALSE
+ ),
+ (
+ 'finite_products_consequences',
+ '["finite-product-preserving"]',
+ '[]',
+ '[]',
+ '["terminal-object-preserving"]',
+ 'This is trivial.',
+ FALSE
+ ),
+ (
+ 'continuous_criterion',
+ '["product-preserving", "equalizer-preserving"]',
+ '["products"]',
+ '[]',
+ '["continuous"]',
+ 'This follows from the construction of limits via equalizers and products, see Mac Lane, Ch. V, Theorem 2.2.',
+ FALSE
+ ),
+ (
+ 'continuous_criterion_filtered',
+ '["left exact", "cofinitary"]',
+ '["finitely complete"]',
+ '[]',
+ '["continuous"]',
+ 'This is because every limit can be written as a filtered limit of finite limits, see Mac Lane, Ch. IX, Theorem 1.1.',
+ FALSE
+ ),
+ (
+ 'product_criterion_filtered',
+ '["finite-product-preserving", "cofinitary"]',
+ '["finite products"]',
+ '[]',
+ '["product-preserving"]',
+ 'This is because every product can be written as a filtered limit of finite products, see Mac Lane, Ch. IX, Theorem 1.1.',
+ FALSE
+ ),
+ (
+ 'exact_definition',
+ '["exact"]',
+ '[]',
+ '[]',
+ '["left exact", "right exact"]',
+ 'This holds by definition.',
+ TRUE
+ ),
+ (
+ 'left_exact_consequences',
+ '["left exact"]',
+ '[]',
+ '[]',
+ '["finite-product-preserving", "terminal-object-preserving"]',
+ 'Both finite products and terminal objects are special cases of finite limits.',
+ FALSE
+ ),
+ (
+ 'left_exact_criterion',
+ '["finite-product-preserving", "equalizer-preserving"]',
+ '["finite products"]',
+ '[]',
+ '["left exact"]',
+ 'This follows from the construction of finite limits via equalizers and finite products, see Mac Lane, Ch. V, Theorem 2.2.',
+ FALSE
+ ),
+ (
+ 'equivalence_consequences',
+ '["equivalence"]',
+ '[]',
+ '[]',
+ '["continuous", "right adjoint", "monadic"]',
+ 'This is easy.',
+ FALSE
+ ),
+ (
+ 'right_adjoint_consequences',
+ '["right adjoint"]',
+ '[]',
+ '[]',
+ '["continuous"]',
+ 'This is standard, see Mac Lane, Ch. V, Theorem 5.1.',
+ FALSE
+ ),
+ (
+ 'saft',
+ '["continuous"]',
+ '["complete", "locally small", "well-powered", "cogenerating set"]',
+ '["locally small"]',
+ '["right adjoint"]',
+ 'This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the nLab, or in Mac Lane, Ch. V, Theorem 8.2.',
+ FALSE
+ ),
+ (
+ 'monadic_consequences',
+ '["monadic"]',
+ '[]',
+ '[]',
+ '["faithful", "right adjoint", "conservative"]',
+ 'This is clear since for a monad $T$ the forgetful functor from the category of $T$-algebras has these properties.',
+ FALSE
+ ),
+ (
+ 'representable_is_continuous',
+ '["representable"]',
+ '[]',
+ '[]',
+ '["continuous"]',
+ 'This is standard, see Mac Lane, Ch. V, Theorem 4.1.',
+ FALSE
+ ),
+ (
+ 'left_exact_preserves_mono',
+ '["left exact"]',
+ '[]',
+ '[]',
+ '["monomorphism-preserving"]',
+ 'This is because $f : X \to Y$ is a monomorphism if and only the square displaying $\mathrm{id}_Y \circ f = \mathrm{id}_Y \circ f$ is a pullback square.',
+ FALSE
+ ),
+ (
+ 'faithful-via-equalizers',
+ '["equalizer-preserving", "conservative"]',
+ '["equalizers"]',
+ '[]',
+ '["faithful"]',
+ 'Let $f,g : X \rightrightarrows Y$ be two morphisms in the source category, and choose an equalizer $E \hookrightarrow X$. By assumption, $F(E) \to F(X)$ is the equalizer of $F(f),F(g) : F(X) \rightrightarrows F(Y)$. Thus, if $F(f) = F(g)$, then $F(E) \to F(X)$ is an isomorphism. Since $F$ is conservative, $E \to X$ is an isomorphism, which means $f = g$.',
+ FALSE
+ ),
+ (
+ 'monadic_full_trivial',
+ '["monadic", "full"]',
+ '[]',
+ '[]',
+ '["equivalence"]',
+ 'Assume that $T$ is a monad on $\mathcal{C}$ such that the forgetful functor $U : \mathbf{Alg}(T) \to \mathcal{C}$ is full. Then by general facts about adjunctions (see MSE/1994963) the unit $\eta : \mathrm{id}_{\mathcal{C}} \to T$ is an isomorphism of functors. Then it is an isomorphism of monads, so that $U$ is an equivalence.',
+ FALSE
+ );
\ No newline at end of file
diff --git a/database/data/008_functors/003_functor-examples.sql b/database/data/008_functors/003_functor-examples.sql
new file mode 100644
index 00000000..8c7ec3d3
--- /dev/null
+++ b/database/data/008_functors/003_functor-examples.sql
@@ -0,0 +1,57 @@
+INSERT INTO functors (
+ id,
+ name,
+ source,
+ target,
+ description,
+ nlab_link
+)
+VALUES
+ (
+ 'id_Set',
+ 'identity functor on the category of sets',
+ 'Set',
+ 'Set',
+ 'Every category $\mathcal{C}$ has an identity functor $\mathrm{id}_{\mathcal{C}}$. Here, we specify that it is for the category of sets.',
+ 'https://ncatlab.org/nlab/show/identity+functor'
+ ),
+ (
+ 'abelianization',
+ 'abelianization functor for groups',
+ 'Grp',
+ 'Ab',
+ 'This functor maps a group $G$ to its abelianization $G^{\mathrm{ab}} := G/[G,G]$.',
+ 'https://ncatlab.org/nlab/show/abelianization'
+ ),
+ (
+ 'forget_vector',
+ 'forgetful functor for vector spaces',
+ 'Vect',
+ 'Set',
+ 'This functor $U$ maps a vector space $V$ (over a fixed field $K$) to its underlying set $U(V)$.',
+ 'https://ncatlab.org/nlab/show/forgetful+functor'
+ ),
+ (
+ 'free_group',
+ 'free group functor',
+ 'Set',
+ 'Grp',
+ 'This functor maps a set $X$ to the free group $F(X)$ on that set.',
+ 'https://ncatlab.org/nlab/show/free+functor'
+ ),
+ (
+ 'power_set_covariant',
+ 'covariant power set functor',
+ 'Set',
+ 'Set',
+ 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.',
+ 'https://ncatlab.org/nlab/show/power+set'
+ ),
+ (
+ 'power_set_contravariant',
+ 'contravariant power set functor',
+ 'Set_op',
+ 'Set',
+ 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$.',
+ 'https://ncatlab.org/nlab/show/power+set'
+ );
\ No newline at end of file
diff --git a/database/data/009_functor-property-assignments/abelianization.sql b/database/data/009_functor-property-assignments/abelianization.sql
new file mode 100644
index 00000000..78d3d595
--- /dev/null
+++ b/database/data/009_functor-property-assignments/abelianization.sql
@@ -0,0 +1,55 @@
+INSERT INTO functor_property_assignments (
+ functor_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'abelianization',
+ 'left adjoint',
+ TRUE,
+ 'This functor is left adjoint to the forgetful functor.'
+),
+(
+ 'abelianization',
+ 'finite-product-preserving',
+ TRUE,
+ 'See MO/386144.'
+),
+(
+ 'abelianization',
+ 'product-preserving',
+ FALSE,
+ 'If $G$ is a group, the canonical homomorphism $(G^{\mathbb{N}})^{\mathrm{ab}} \to (G^{\mathrm{ab}})^{\mathbb{N}}$ is surjective, but does not need to be an isomorphism: otherwise, the inclusion $[G^{\mathbb{N}}, G^{\mathbb{N}}] \subseteq [G,G]^{\mathbb{N}}$ would be an equality. But this requires the commutator width of $G$ to be finite, which fails for $G = F_2$ for instance. See also The abelianization of inverse limits of groups, Remark 0.0.7.'
+),
+(
+ 'abelianization',
+ 'monomorphism-preserving',
+ FALSE,
+ 'The monomorphism $A_3 \hookrightarrow S_3$ is mapped to $A_3 \to 1$.'
+),
+(
+ 'abelianization',
+ 'essentially surjective',
+ TRUE,
+ 'For abelian groups $G$ we have $G \cong G^{\mathrm{ab}}$.'
+),
+(
+ 'abelianization',
+ 'faithful',
+ FALSE,
+ 'Both the inclusion $A_3 \hookrightarrow S_3$ and the trivial homomorphism $A_3 \to S_3$ are mapped to the trivial homomorphism $A_3 \to 1$.'
+),
+(
+ 'abelianization',
+ 'conservative',
+ FALSE,
+ 'The proper inclusion $S_3 \hookrightarrow S_4$ gets mapped to the trivial homomorphism $1 \to 1$, which is an isomorphism.'
+),
+(
+ 'abelianization',
+ 'full',
+ FALSE,
+ 'See MSE/716686.'
+);
\ No newline at end of file
diff --git a/database/data/009_functor-property-assignments/forget_vector.sql b/database/data/009_functor-property-assignments/forget_vector.sql
new file mode 100644
index 00000000..58eee97a
--- /dev/null
+++ b/database/data/009_functor-property-assignments/forget_vector.sql
@@ -0,0 +1,55 @@
+INSERT INTO functor_property_assignments (
+ functor_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'forget_vector',
+ 'representable',
+ TRUE,
+ 'This functor is represented by any $1$-dimensional vector space.'
+),
+(
+ 'forget_vector',
+ 'conservative',
+ TRUE,
+ 'It is standard that the inverse of a bijective linear map is also linear.'
+),
+(
+ 'forget_vector',
+ 'finitary',
+ TRUE,
+ 'For every algebraic category the forgetful functor to the category of sets preserves filtered colimits.'
+),
+(
+ 'forget_vector',
+ 'monadic',
+ TRUE,
+ 'For every algebraic category the forgetful functor to the category of sets is monadic.'
+),
+(
+ 'forget_vector',
+ 'epimorphism-preserving',
+ TRUE,
+ 'This follows from the classifications of epimorphisms in the category of vector spaces and in the category of sets.'
+),
+(
+ 'forget_vector',
+ 'initial-object-preserving',
+ FALSE,
+ 'The underlying set of a trivial vector space is not empty.'
+),
+(
+ 'forget_vector',
+ 'essentially surjective',
+ FALSE,
+ 'The empty has has no vector space structure.'
+),
+(
+ 'forget_vector',
+ 'coequalizer-preserving',
+ FALSE,
+ 'The coequalizer of $0,i_1 : K \to K^2$ in $\mathbf{Vect}$ is $p_2 : K^2 \to K$, but the coequalizer in $\mathbf{Set}$ is $(K \times K^*) \cup \{(0,0)\}$.'
+);
\ No newline at end of file
diff --git a/database/data/009_functor-property-assignments/free_group.sql b/database/data/009_functor-property-assignments/free_group.sql
new file mode 100644
index 00000000..924b2775
--- /dev/null
+++ b/database/data/009_functor-property-assignments/free_group.sql
@@ -0,0 +1,55 @@
+INSERT INTO functor_property_assignments (
+ functor_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'free_group',
+ 'left adjoint',
+ TRUE,
+ 'This functor is left adjoint to the forgetful functor.'
+),
+(
+ 'free_group',
+ 'monomorphism-preserving',
+ TRUE,
+ 'This can be deduced from the description of the elements of a free group, but here is an abstract argument: Split monomorphisms are preserved by any functor. The only injective maps in $\mathbf{Set}$ that are not split are $\emptyset \hookrightarrow X$ (for non-empty $X$), and $F(\emptyset) \to F(X)$ is injective since $F(\emptyset)$ is the trivial group.'
+),
+(
+ 'free_group',
+ 'faithful',
+ TRUE,
+ 'A left adjoint is faithful if and only if its unit consists of monomorphisms. So we only need to check that every set embeds into (the underlying set of) its free group. But this is clear since $X$ already embeds into the free abelian group $\mathbb{Z}^{\oplus X}$, which is a quotient of the free group.'
+),
+(
+ 'free_group',
+ 'conservative',
+ TRUE,
+ 'Let $f : X \to Y$ be a map of sets such that $F(f) : F(X) \to F(Y)$ is an isomorphism of groups. We know that $F$ is faithful, so that it reflects monomorphisms. Thus, $f$ is injective. Choose a complement $U \subseteq Y$ of $f(X) \subseteq Y$. Then $F(X) \to F(Y) = F(X) \sqcup F(U)$ is an isomorphism. This implies $F(U)=1$ and hence $U = \emptyset$.'
+),
+(
+ 'free_group',
+ 'essentially surjective',
+ FALSE,
+ 'Not every group is free (consider $\mathbb{Z}/2$).'
+),
+(
+ 'free_group',
+ 'terminal-object-preserving',
+ FALSE,
+ 'The free group of rank $1$ is not the trivial group.'
+),
+(
+ 'free_group',
+ 'full',
+ FALSE,
+ 'The map $1 = \mathrm{Hom}(1,1) \to \mathrm{Hom}(F(1),F(1)) = \mathrm{Hom}(\mathbb{Z},\mathbb{Z}) = \mathbb{Z}$ is not surjective.'
+),
+(
+ 'free_group',
+ 'equalizer-preserving',
+ FALSE,
+ 'Let $f,g : \{a,b\} \rightrightarrows \{c,d\}$ be the two constant maps, $f \equiv c$, $g \equiv d$. Their equalizer is empty, and the free group on that equalizer is trivial. Now consider the induced group homomorphisms $F(f), F(g) : F(\{a,b\}) \rightrightarrows F(\{c,d\})$ and observe that $a \cdot b^{-1}$ lies in the kernel of both homomorphisms, hence in their equalizer.'
+);
diff --git a/database/data/009_functor-property-assignments/id_Set.sql b/database/data/009_functor-property-assignments/id_Set.sql
new file mode 100644
index 00000000..3264a7f3
--- /dev/null
+++ b/database/data/009_functor-property-assignments/id_Set.sql
@@ -0,0 +1,19 @@
+INSERT INTO functor_property_assignments (
+ functor_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'id_Set',
+ 'equivalence',
+ TRUE,
+ 'This is trivial.'
+),
+(
+ 'id_Set',
+ 'representable',
+ TRUE,
+ 'This functor is represented by any singleton set.'
+);
\ No newline at end of file
diff --git a/database/data/009_functor-property-assignments/power_set_contravariant.sql b/database/data/009_functor-property-assignments/power_set_contravariant.sql
new file mode 100644
index 00000000..2ceb93eb
--- /dev/null
+++ b/database/data/009_functor-property-assignments/power_set_contravariant.sql
@@ -0,0 +1,55 @@
+INSERT INTO functor_property_assignments (
+ functor_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'power_set_contravariant',
+ 'representable',
+ TRUE,
+ 'This is because there are natural bijections $P(X) \cong \mathrm{Hom}(X,2)$, sending a subset to its characteristic function.'
+),
+(
+ 'power_set_contravariant',
+ 'monadic',
+ TRUE,
+ 'See Johnstone, Theorem 2.2.7.'
+),
+(
+ 'power_set_contravariant',
+ 'epimorphism-preserving',
+ TRUE,
+ 'If $f : X \to Y$ is injective, then $f^* : P(Y) \to P(X)$ is surjective, since for all $A \subseteq X$ we have $A = f^*(f_*(A))$.'
+),
+(
+ 'power_set_contravariant',
+ 'coequalizer-preserving',
+ FALSE,
+ 'The power set functor preserves reflexive coequalizers, but not all coequalizers, i.e. there are maps $f,g : Y \to X$ with equalizer $E \subseteq Y$ such that $P(Y) \twoheadrightarrow P(E)$ is not the coequalizer of $f^*,g^* : P(X) \to P(Y)$: Let $X=\{0,1\}$ and $Y=\{a,b,c\}$. Define maps $f,g:Y\to X$ by $f(a)=0$, $f(b)=0$, $f(c)=1$ and $g(a)=0$, $g(b)=1$, $g(c)=0$. Their equalizer is $E = \{a\}$, so that $P(E)$ has $2$ elements. For $S=\{0\}$ one has $f^*(S)=\{a,b\}$, $g^*(S)=\{a,c\}$, and for $S=\{1\}$ one has $f^*(S)=\{c\}$, $g^*(S)=\{b\}$. Thus the coequalizer of $f^*,g^*$ is obtained from $P(Y)$ by imposing the two relations $\{a,b\} \sim \{a,c\}$ and $\{c\} \sim \{b\}$. But then it as $8-2 = 6$ elements.'
+),
+(
+ 'power_set_contravariant',
+ 'initial-object-preserving',
+ FALSE,
+ 'In fact, the initial object does not even lie in the essential image since $P(X) \neq 0$ for all $X$.'
+),
+(
+ 'power_set_contravariant',
+ 'finitary',
+ FALSE,
+ 'Consider the sequence of projections $\cdots \twoheadrightarrow \{0,1\}^2 \twoheadrightarrow \{0,1\}^1$. Its limit in $\mathbf{Set}$ (i.e. colimit in $\mathbf{Set}^{\mathrm{op}}$) is $\{0,1\}^{\mathbb{N}}$, which is uncountable, so that $P(\{0,1\}^{\mathbb{N}})$ is also uncountable. But the colimit of the induced diagram $P(\{0,1\}^1) \hookrightarrow P(\{0,1\}^2) \hookrightarrow \cdots$ is countable since each $P(\{0,1\}^n)$ is finite.'
+),
+(
+ 'power_set_contravariant',
+ 'essentially surjective',
+ FALSE,
+ 'The initial object does not lie in the essential image since $P(X) \neq 0$ for all $X$.'
+),
+(
+ 'power_set_contravariant',
+ 'full',
+ FALSE,
+ 'The maps $f^* : P(Y) \to P(X)$ preserve the empty set, so take the constant map $P(X) \to P(X)$, $T \mapsto X$ for instance (where $X$ is non-empty).'
+);
diff --git a/database/data/009_functor-property-assignments/power_set_covariant.sql b/database/data/009_functor-property-assignments/power_set_covariant.sql
new file mode 100644
index 00000000..50036ab1
--- /dev/null
+++ b/database/data/009_functor-property-assignments/power_set_covariant.sql
@@ -0,0 +1,73 @@
+INSERT INTO functor_property_assignments (
+ functor_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'power_set_covariant',
+ 'monomorphism-preserving',
+ TRUE,
+ 'If $f : X \to Y$ is injective, then $f^* \circ f_* = \mathrm{id}_{P(X)}$, so that $f_*$ is injective.'
+),
+(
+ 'power_set_covariant',
+ 'epimorphism-preserving',
+ TRUE,
+ 'If $f : X \to Y$ is surjective, then $f_* \circ f^* = \mathrm{id}_{P(Y)}$, so that $f^*$ is surjective.'
+),
+(
+ 'power_set_covariant',
+ 'faithful',
+ TRUE,
+ 'Let $f,g : X \rightrightarrows Y$ be two maps with $f_* = g_* : P(X) \rightrightarrows P(Y)$. Then $\{f(x)\} = f_*(\{x\}) = g_*(\{x\}) = \{g(x)\}$ and hence $f(x) = g(x)$ for all $x \in X$.'
+),
+(
+ 'power_set_covariant',
+ 'conservative',
+ TRUE,
+ 'Assume that $f : X \to Y$ is a map such that $f_* : P(X) \to P(Y)$ is an isomorphism. There is some $A \subseteq X$ with $Y = f_*(A)$, this proves that $f$ is surjective. It is also injective: If $x,y \in X$ satisfy $f(x) = f(y)$, then $f_*(\{x\}) = f_*(\{y\})$, and hence $\{x\} = \{y\}$, i.e. $x = y$.'
+),
+(
+ 'power_set_covariant',
+ 'full',
+ FALSE,
+ 'Take any map $P(X) \to P(X)$ that does not preserve the empty set, say the constant map with value $X$ (for $X \neq \emptyset$).'
+),
+(
+ 'power_set_covariant',
+ 'terminal-object-preserving',
+ FALSE,
+ 'We have $2^1 \neq 1$.'
+),
+(
+ 'power_set_covariant',
+ 'initial-object-preserving',
+ FALSE,
+ 'We have $2^0 \neq 0$.'
+),
+(
+ 'power_set_covariant',
+ 'essentially surjective',
+ FALSE,
+ 'Every power set is non-empty.'
+),
+(
+ 'power_set_covariant',
+ 'finitary',
+ FALSE,
+ 'The filtered colimit $\mathbb{N} = \bigcup_{n \geq 0} \mathbb{N}_{\leq n}$ is not preserved by $P$, since $\bigcup_{n \geq 0} P(\mathbb{N}_{\leq n})$ just consists of the finite subsets of $\mathbb{N}$.'
+),
+(
+ 'power_set_covariant',
+ 'equalizer-preserving',
+ FALSE,
+ 'Any pair of distinct surjective maps $f,g : X \rightrightarrows Y$ provides a counterexample: Their equalizer $E$ is a proper subset of $X$, so that $P(E)$ cannot contain $X$. But $f_*(X) = Y = g_*(X)$ shows that $X$ is contained in the equalizer of $f_*,g_* : P(X) \rightrightarrows P(Y)$.'
+),
+(
+ 'power_set_covariant',
+ 'coequalizer-preserving',
+ FALSE,
+ 'Let $X := \{x,y\}$. Consider the two maps $x,y : \{0\} \rightrightarrows X$. Their coequalizer $Q = X / (x = y)$ has just one element, so that $P(Q)$ has two elements. The induced maps $x_*,y_* : P(\{0\}) \rightrightarrows P(X)$ (which already agree on the empty set) have coequalizer $P(X) / (\{x\} = \{y\})$, which has $3$ elements. So it cannot be $P(Q)$.'
+);
diff --git a/database/migrations/010_functors-table.sql b/database/migrations/010_functors-table.sql
new file mode 100644
index 00000000..e69bb02b
--- /dev/null
+++ b/database/migrations/010_functors-table.sql
@@ -0,0 +1,10 @@
+CREATE TABLE functors (
+ id TEXT PRIMARY KEY,
+ name TEXT NOT NULL UNIQUE,
+ source TEXT NOT NULL,
+ target TEXT NOT NULL,
+ description TEXT NOT NULL CHECK (length(description) > 0),
+ nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'),
+ FOREIGN KEY (source) REFERENCES categories (id) ON DELETE CASCADE,
+ FOREIGN KEY (target) REFERENCES categories (id) ON DELETE CASCADE
+);
\ No newline at end of file
diff --git a/database/migrations/011_functor-properties-tables.sql b/database/migrations/011_functor-properties-tables.sql
new file mode 100644
index 00000000..605aee8f
--- /dev/null
+++ b/database/migrations/011_functor-properties-tables.sql
@@ -0,0 +1,22 @@
+CREATE TABLE functor_properties (
+ id TEXT PRIMARY KEY,
+ relation TEXT NOT NULL,
+ description TEXT NOT NULL CHECK (length(description) > 0),
+ nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'),
+ invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE,
+ dual_property_id TEXT,
+ FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT,
+ FOREIGN KEY (dual_property_id) REFERENCES functor_properties (id) ON DELETE SET NULL
+);
+
+CREATE TABLE functor_property_assignments (
+ functor_id TEXT NOT NULL,
+ property_id TEXT NOT NULL,
+ is_satisfied INTEGER NOT NULL CHECK (is_satisfied IN (TRUE, FALSE)),
+ reason TEXT NOT NULL CHECK (length(reason) > 0),
+ is_deduced INTEGER NOT NULL DEFAULT FALSE CHECK (is_deduced in (TRUE, FALSE)),
+ position INTEGER NOT NULL DEFAULT 0,
+ PRIMARY KEY (functor_id, property_id),
+ FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE,
+ FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE
+);
\ No newline at end of file
diff --git a/database/migrations/012_functor-implications.sql b/database/migrations/012_functor-implications.sql
new file mode 100644
index 00000000..853b7e04
--- /dev/null
+++ b/database/migrations/012_functor-implications.sql
@@ -0,0 +1,51 @@
+CREATE TABLE functor_implications (
+ id TEXT PRIMARY KEY,
+ reason TEXT NOT NULL CHECK (length(reason) > 0),
+ is_deduced INTEGER NOT NULL DEFAULT FALSE,
+ dualized_from TEXT,
+ is_equivalence INTEGER NOT NULL DEFAULT FALSE,
+ CHECK (dualized_from IS NULL OR is_deduced = TRUE),
+ FOREIGN KEY (dualized_from) REFERENCES functor_implications (id) ON DELETE SET NULL
+);
+
+CREATE TABLE functor_implication_assumptions (
+ implication_id TEXT NOT NULL,
+ property_id TEXT NOT NULL,
+ PRIMARY KEY (implication_id, property_id),
+ FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE,
+ FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE
+);
+
+CREATE TABLE functor_implication_conclusions (
+ implication_id TEXT NOT NULL,
+ property_id TEXT NOT NULL,
+ PRIMARY KEY (implication_id, property_id),
+ FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE,
+ FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE
+);
+
+-- property of source category
+CREATE TABLE functor_implication_source_assumptions (
+ implication_id TEXT NOT NULL,
+ property_id TEXT NOT NULL,
+ PRIMARY KEY (implication_id, property_id),
+ FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE,
+ FOREIGN KEY (property_id) REFERENCES properties (id) ON DELETE CASCADE
+);
+
+-- property of target category
+CREATE TABLE functor_implication_target_assumptions (
+ implication_id TEXT NOT NULL,
+ property_id TEXT NOT NULL,
+ PRIMARY KEY (implication_id, property_id),
+ FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE,
+ FOREIGN KEY (property_id) REFERENCES properties (id) ON DELETE CASCADE
+);
+
+CREATE INDEX idx_assumptions_functor_property ON functor_implication_assumptions (property_id);
+
+CREATE INDEX idx_conclusions_functor_property ON functor_implication_conclusions (property_id);
+
+CREATE INDEX idx_assumptions_functor_source_property ON functor_implication_source_assumptions (property_id);
+
+CREATE INDEX idx_conclusions_functor_target_property ON functor_implication_target_assumptions (property_id);
\ No newline at end of file
diff --git a/database/migrations/013_functor-implication-view.sql b/database/migrations/013_functor-implication-view.sql
new file mode 100644
index 00000000..4dee59f9
--- /dev/null
+++ b/database/migrations/013_functor-implication-view.sql
@@ -0,0 +1,83 @@
+CREATE VIEW functor_implications_view AS
+SELECT
+ i.id,
+ i.is_equivalence,
+ i.reason,
+ i.is_deduced,
+ i.dualized_from,
+ (
+ SELECT json_group_array(property_id) FROM (
+ SELECT property_id
+ FROM functor_implication_assumptions a
+ WHERE a.implication_id = i.id
+ ORDER BY lower(property_id)
+ )
+ ) AS assumptions,
+ (
+ SELECT json_group_array(property_id) FROM (
+ SELECT property_id
+ FROM functor_implication_source_assumptions a
+ WHERE a.implication_id = i.id
+ ORDER BY lower(property_id)
+ )
+ ) AS source_assumptions,
+ (
+ SELECT json_group_array(property_id) FROM (
+ SELECT property_id
+ FROM functor_implication_target_assumptions a
+ WHERE a.implication_id = i.id
+ ORDER BY lower(property_id)
+ )
+ ) AS target_assumptions,
+ (
+ SELECT json_group_array(property_id) FROM (
+ SELECT property_id
+ FROM functor_implication_conclusions c
+ WHERE c.implication_id = i.id
+ ORDER BY lower(property_id)
+ )
+ ) AS conclusions
+FROM functor_implications i;
+
+
+CREATE VIEW functor_implication_input AS
+SELECT
+ NULL AS id,
+ NULL AS is_equivalence,
+ NULL AS assumptions,
+ NULL AS source_assumptions,
+ NULL AS target_assumptions,
+ NULL AS conclusions,
+ NULL AS reason,
+ NULL AS is_deduced,
+ NULL AS dualized_from;
+
+
+CREATE TRIGGER trg_functor_implication_input_insert
+INSTEAD OF INSERT ON functor_implication_input
+BEGIN
+ INSERT INTO functor_implications (id, reason, is_equivalence, is_deduced, dualized_from)
+ VALUES (
+ NEW.id,
+ NEW.reason,
+ COALESCE(NEW.is_equivalence, FALSE),
+ COALESCE(NEW.is_deduced, FALSE),
+ NEW.dualized_from
+ );
+
+ INSERT INTO functor_implication_assumptions (implication_id, property_id)
+ SELECT NEW.id, value
+ FROM json_each(NEW.assumptions);
+
+ INSERT INTO functor_implication_source_assumptions (implication_id, property_id)
+ SELECT NEW.id, value
+ FROM json_each(NEW.source_assumptions);
+
+ INSERT INTO functor_implication_target_assumptions (implication_id, property_id)
+ SELECT NEW.id, value
+ FROM json_each(NEW.target_assumptions);
+
+ INSERT INTO functor_implication_conclusions (implication_id, property_id)
+ SELECT NEW.id, value
+ FROM json_each(NEW.conclusions);
+END;
\ No newline at end of file
diff --git a/scripts/deduce-implications.ts b/scripts/deduce-category-implications.ts
similarity index 82%
rename from scripts/deduce-implications.ts
rename to scripts/deduce-category-implications.ts
index 96acf5cc..60b98d3d 100644
--- a/scripts/deduce-implications.ts
+++ b/scripts/deduce-category-implications.ts
@@ -1,20 +1,20 @@
import { type Client } from '@libsql/client'
-import { are_equal_sets } from './utils'
+import { are_equal_sets } from './shared'
import dotenv from 'dotenv'
dotenv.config({ quiet: true })
-export async function deduce_implications(db: Client) {
- await clear_deduced_implications(db)
- await create_dualized_implications(db)
- await create_self_dual_implications(db)
+export async function deduce_category_implications(db: Client) {
+ await clear_deduced_category_implications(db)
+ await create_dualized_category_implications(db)
+ await create_self_dual_category_implications(db)
}
-async function clear_deduced_implications(db: Client) {
+async function clear_deduced_category_implications(db: Client) {
await db.execute(`DELETE FROM implications WHERE is_deduced = TRUE`)
}
-async function create_dualized_implications(db: Client) {
+async function create_dualized_category_implications(db: Client) {
const res = await db.execute(`
SELECT
v.id,
@@ -88,10 +88,10 @@ async function create_dualized_implications(db: Client) {
'write',
)
- console.info(`Dualized ${dualizable_implications.length} implications`)
+ console.info(`Dualized ${dualizable_implications.length} category implications`)
}
-async function create_self_dual_implications(db: Client) {
+async function create_self_dual_category_implications(db: Client) {
const { rows } = await db.execute(`
INSERT INTO implication_input (
id,
@@ -118,5 +118,5 @@ async function create_self_dual_implications(db: Client) {
RETURNING id
`)
- console.info(`Created ${rows.length} self-dual implications`)
+ console.info(`Created ${rows.length} self-dual category implications`)
}
diff --git a/scripts/deduce-properties.ts b/scripts/deduce-category-properties.ts
similarity index 69%
rename from scripts/deduce-properties.ts
rename to scripts/deduce-category-properties.ts
index 08a217ef..00a54e6c 100644
--- a/scripts/deduce-properties.ts
+++ b/scripts/deduce-category-properties.ts
@@ -3,9 +3,9 @@ import dotenv from 'dotenv'
import {
get_assumption_string,
get_conclusion_string,
- get_normalized_implications,
- NormalizedImplication,
-} from './implication.utils'
+ is_subset,
+ NormalizedCategoryImplication,
+} from './shared'
dotenv.config({ quiet: true })
@@ -15,23 +15,22 @@ type CategoryMeta = {
dual_category_id: string | null
}
-export async function deduce_all_properties(db: Client) {
+export async function deduce_category_properties(db: Client) {
const tx = await db.transaction()
try {
- const implications = await get_normalized_implications(tx)
- if (!implications) return
+ const implications = await get_normalized_category_implications(tx)
const categories = await get_categories(tx)
for (const category of categories) {
- await delete_deduced_properties(tx, category.id)
- await deduce_satisfied_properties(tx, category.id, implications)
- await deduce_unsatisfied_properties(tx, category.id, implications)
+ await delete_deduced_category_properties(tx, category.id)
+ await deduce_satisfied_category_properties(tx, category.id, implications)
+ await deduce_unsatisfied_category_properties(tx, category.id, implications)
}
for (const category of categories) {
- await deduce_dual_properties(tx, category)
+ await deduce_dual_category_properties(tx, category)
}
await tx.commit()
@@ -42,6 +41,66 @@ export async function deduce_all_properties(db: Client) {
}
}
+async function get_normalized_category_implications(
+ tx: Transaction,
+): Promise {
+ const res = await tx.execute(`
+ SELECT
+ v.id,
+ v.assumptions,
+ v.conclusions,
+ v.is_equivalence,
+ (
+ SELECT json_group_object(p.id, p.relation)
+ FROM properties p
+ WHERE p.id IN (
+ SELECT value FROM json_each(v.assumptions)
+ UNION
+ SELECT value FROM json_each(v.conclusions)
+ )
+ ) AS relations
+ FROM implications_view v
+ `)
+
+ const all_implications_db = res.rows as unknown as {
+ id: string
+ assumptions: string
+ conclusions: string
+ is_equivalence: number
+ relations: string
+ }[]
+
+ const implications: NormalizedCategoryImplication[] = []
+
+ for (const impl of all_implications_db) {
+ const assumptions: string[] = JSON.parse(impl.assumptions)
+ const conclusions: string[] = JSON.parse(impl.conclusions)
+ const relations: Record = JSON.parse(impl.relations)
+
+ for (const conclusion of conclusions) {
+ implications.push({
+ id: impl.id,
+ assumptions: new Set(assumptions),
+ conclusion,
+ relations,
+ })
+ }
+
+ if (impl.is_equivalence) {
+ for (const assumption of assumptions) {
+ implications.push({
+ id: impl.id,
+ assumptions: new Set(conclusions),
+ conclusion: assumption,
+ relations,
+ })
+ }
+ }
+ }
+
+ return implications
+}
+
async function get_categories(tx: Transaction) {
const res = await tx.execute(`
SELECT id, name, dual_category_id
@@ -50,7 +109,7 @@ async function get_categories(tx: Transaction) {
return res.rows as unknown as CategoryMeta[]
}
-async function delete_deduced_properties(tx: Transaction, category_id: string) {
+async function delete_deduced_category_properties(tx: Transaction, category_id: string) {
await tx.execute({
sql: `
DELETE FROM category_property_assignments
@@ -60,46 +119,10 @@ async function delete_deduced_properties(tx: Transaction, category_id: string) {
})
}
-async function deduce_dual_properties(tx: Transaction, category: CategoryMeta) {
- const allowed =
- category.dual_category_id !== null &&
- category.name.toLowerCase().startsWith('dual') // prevent circular deduction
-
- if (!allowed) return
-
- const res = await tx.execute({
- sql: `
- INSERT OR REPLACE INTO category_property_assignments
- (category_id, property_id, is_satisfied, reason, is_deduced)
- SELECT
- ?,
- p.dual_property_id,
- a.is_satisfied,
- CASE
- WHEN a.is_satisfied THEN
- 'Its dual category ' || r.relation || ' ' || a.property_id || '.'
- ELSE
- 'Its dual category ' || r.negation || ' ' || a.property_id || '.'
- END,
- TRUE
- FROM category_property_assignments a
- INNER JOIN properties p ON p.id = a.property_id
- INNER JOIN relations r ON r.relation= p.relation
- WHERE a.category_id = ? AND p.dual_property_id IS NOT NULL
- ORDER BY lower(p.dual_property_id)
- `,
- args: [category.id, category.dual_category_id],
- })
-
- console.info(
- `Added ${res.rowsAffected} (un-)satisfied properties for ${category.id} to the database by using its dual ${category.dual_category_id}`,
- )
-}
-
-async function deduce_satisfied_properties(
+async function deduce_satisfied_category_properties(
tx: Transaction,
category_id: string,
- implications: NormalizedImplication[],
+ implications: NormalizedCategoryImplication[],
) {
const satisfied_res = await tx.execute({
sql: `
@@ -123,7 +146,7 @@ async function deduce_satisfied_properties(
while (true) {
const implication = implications.find(
({ assumptions, conclusion }) =>
- [...assumptions].every((p) => satisfied_props.has(p)) &&
+ is_subset(assumptions, satisfied_props) &&
!satisfied_props.has(conclusion),
)
if (!implication) break
@@ -164,14 +187,14 @@ async function deduce_satisfied_properties(
}
console.info(
- `Added ${deduced_satisfied_props.length} satisfied properties for ${category_id} to the database`,
+ `Added ${deduced_satisfied_props.length} satisfied properties for category ${category_id} to the database`,
)
}
-async function deduce_unsatisfied_properties(
+async function deduce_unsatisfied_category_properties(
tx: Transaction,
category_id: string,
- implications: NormalizedImplication[],
+ implications: NormalizedCategoryImplication[],
) {
const satisfied_res = await tx.execute({
sql: `
@@ -211,9 +234,7 @@ async function deduce_unsatisfied_properties(
for (const p of implication.assumptions) {
const is_valid =
!unsatisfied_props.has(p) &&
- [...implication.assumptions].every(
- (q) => q === p || satisfied_props.has(q),
- )
+ is_subset(implication.assumptions, satisfied_props, p)
if (is_valid) return { implication, property: p }
}
}
@@ -268,6 +289,42 @@ async function deduce_unsatisfied_properties(
}
console.info(
- `Added ${deduced_unsatisfied_props.length} unsatisfied properties for ${category_id} to the database`,
+ `Added ${deduced_unsatisfied_props.length} unsatisfied properties for category ${category_id} to the database`,
+ )
+}
+
+async function deduce_dual_category_properties(tx: Transaction, category: CategoryMeta) {
+ const allowed =
+ category.dual_category_id !== null &&
+ category.name.toLowerCase().startsWith('dual') // prevent circular deduction
+
+ if (!allowed) return
+
+ const res = await tx.execute({
+ sql: `
+ INSERT OR REPLACE INTO category_property_assignments
+ (category_id, property_id, is_satisfied, reason, is_deduced)
+ SELECT
+ ?,
+ p.dual_property_id,
+ a.is_satisfied,
+ CASE
+ WHEN a.is_satisfied THEN
+ 'Its dual category ' || r.relation || ' ' || a.property_id || '.'
+ ELSE
+ 'Its dual category ' || r.negation || ' ' || a.property_id || '.'
+ END,
+ TRUE
+ FROM category_property_assignments a
+ INNER JOIN properties p ON p.id = a.property_id
+ INNER JOIN relations r ON r.relation= p.relation
+ WHERE a.category_id = ? AND p.dual_property_id IS NOT NULL
+ ORDER BY lower(p.dual_property_id)
+ `,
+ args: [category.id, category.dual_category_id],
+ })
+
+ console.info(
+ `Added ${res.rowsAffected} (un-)satisfied properties for category ${category.id} to the database by using its dual ${category.dual_category_id}`,
)
}
diff --git a/scripts/deduce-functor-implications.ts b/scripts/deduce-functor-implications.ts
new file mode 100644
index 00000000..c5a523ba
--- /dev/null
+++ b/scripts/deduce-functor-implications.ts
@@ -0,0 +1,111 @@
+import { type Client } from '@libsql/client'
+import { are_equal_sets } from './shared'
+import dotenv from 'dotenv'
+
+dotenv.config({ quiet: true })
+
+// TODO: remove code duplication with category implication deduction script
+
+export async function deduce_functor_implications(db: Client) {
+ await clear_deduced_functor_implications(db)
+ await create_dualized_functor_implications(db)
+}
+
+async function clear_deduced_functor_implications(db: Client) {
+ await db.execute(`DELETE FROM functor_implications WHERE is_deduced = TRUE`)
+}
+
+async function create_dualized_functor_implications(db: Client) {
+ const res = await db.execute(`
+ SELECT
+ v.id,
+ v.assumptions,
+ v.conclusions,
+ v.is_equivalence,
+ v.reason,
+ (
+ SELECT json_group_array(p.dual_property_id)
+ FROM json_each(v.assumptions) a
+ JOIN functor_properties p ON p.id = a.value
+ ) AS dual_assumptions,
+ (
+ SELECT json_group_array(p.dual_property_id)
+ FROM json_each(v.source_assumptions) sa
+ JOIN properties p ON p.id = sa.value
+ ) AS dual_source_assumptions,
+ (
+ SELECT json_group_array(p.dual_property_id)
+ FROM json_each(v.target_assumptions) ta
+ JOIN properties p ON p.id = ta.value
+ ) AS dual_target_assumptions,
+ (
+ SELECT json_group_array(p.dual_property_id)
+ FROM json_each(v.conclusions) c
+ JOIN functor_properties p ON p.id = c.value
+ ) AS dual_conclusions
+ FROM functor_implications_view v
+ WHERE v.is_deduced = FALSE
+ `)
+
+ const implications = res.rows as unknown as {
+ id: string
+ assumptions: string
+ conclusions: string
+ dual_assumptions: string
+ dual_source_assumptions: string
+ dual_target_assumptions: string
+ dual_conclusions: string
+ is_equivalence: number
+ reason: string
+ }[]
+
+ const dualizable_implications = implications.filter((impl) => {
+ const has_null =
+ JSON.parse(impl.dual_assumptions).includes(null) ||
+ JSON.parse(impl.dual_conclusions).includes(null) ||
+ JSON.parse(impl.dual_source_assumptions).includes(null) ||
+ JSON.parse(impl.dual_target_assumptions).includes(null)
+
+ if (has_null) return false
+
+ const assumptions = new Set(JSON.parse(impl.assumptions))
+ const conclusions = new Set(JSON.parse(impl.conclusions))
+ const dual_assumptions = new Set(JSON.parse(impl.dual_assumptions))
+ const dual_conclusions = new Set(JSON.parse(impl.dual_conclusions))
+
+ return (
+ !are_equal_sets(assumptions, dual_assumptions) ||
+ !are_equal_sets(conclusions, dual_conclusions)
+ )
+ })
+
+ await db.batch(
+ dualizable_implications.map((impl) => ({
+ sql: `
+ INSERT INTO functor_implication_input (
+ id,
+ assumptions,
+ source_assumptions,
+ target_assumptions,
+ conclusions,
+ is_equivalence,
+ reason,
+ dualized_from,
+ is_deduced
+ ) VALUES (?, ?, ?, ?, ?, ?, ?, ?, TRUE)`,
+ args: [
+ `dual_${impl.id}`,
+ impl.dual_assumptions,
+ impl.dual_source_assumptions,
+ impl.dual_target_assumptions,
+ impl.dual_conclusions,
+ impl.is_equivalence,
+ 'This follows from the dual implication.',
+ impl.id,
+ ],
+ })),
+ 'write',
+ )
+
+ console.info(`Dualized ${dualizable_implications.length} functor implications`)
+}
diff --git a/scripts/deduce-functor-properties.ts b/scripts/deduce-functor-properties.ts
new file mode 100644
index 00000000..081e2697
--- /dev/null
+++ b/scripts/deduce-functor-properties.ts
@@ -0,0 +1,338 @@
+import type { Transaction, Client } from '@libsql/client'
+import dotenv from 'dotenv'
+import {
+ get_assumption_string,
+ get_conclusion_string,
+ is_subset,
+ NormalizedFunctorImplication,
+} from './shared'
+
+dotenv.config({ quiet: true })
+
+type FunctorMeta = {
+ id: string
+ name: string
+ source: string
+ source_props: Set
+ target: string
+ target_props: Set
+}
+
+// TODO: remove code duplication with category deduction script
+// (not quite the same because we need source and target assumptions)
+
+export async function deduce_functor_properties(db: Client) {
+ const tx = await db.transaction()
+
+ try {
+ const implications = await get_normalized_functor_implications(tx)
+
+ const functors = await get_functors(tx)
+
+ for (const functor of functors) {
+ await delete_deduced_functor_properties(tx, functor)
+ await deduce_satisfied_functor_properties(tx, functor, implications)
+ await deduce_unsatisfied_functor_properties(tx, functor, implications)
+ }
+
+ await tx.commit()
+ } catch (err) {
+ console.error(err)
+ await tx.rollback()
+ throw err
+ }
+}
+
+async function get_normalized_functor_implications(
+ tx: Transaction,
+): Promise {
+ const res = await tx.execute(`
+ SELECT
+ v.id,
+ v.assumptions,
+ v.source_assumptions,
+ v.target_assumptions,
+ v.conclusions,
+ v.is_equivalence,
+ (
+ SELECT json_group_object(p.id, p.relation)
+ FROM functor_properties p
+ WHERE p.id IN (
+ SELECT value FROM json_each(v.assumptions)
+ UNION
+ SELECT value FROM json_each(v.conclusions)
+ )
+ ) AS relations
+ FROM functor_implications_view v
+ `)
+
+ const all_implications_db = res.rows as unknown as {
+ id: string
+ assumptions: string
+ source_assumptions: string
+ target_assumptions: string
+ conclusions: string
+ is_equivalence: number
+ relations: string
+ }[]
+
+ const implications: NormalizedFunctorImplication[] = []
+
+ for (const impl of all_implications_db) {
+ const assumptions: string[] = JSON.parse(impl.assumptions)
+ const conclusions: string[] = JSON.parse(impl.conclusions)
+ const source_assumptions: string[] = JSON.parse(impl.source_assumptions)
+ const target_assumptions: string[] = JSON.parse(impl.target_assumptions)
+ const relations: Record = JSON.parse(impl.relations)
+
+ for (const conclusion of conclusions) {
+ implications.push({
+ id: impl.id,
+ assumptions: new Set(assumptions),
+ source_assumptions: new Set(source_assumptions),
+ target_assumptions: new Set(target_assumptions),
+ conclusion,
+ relations,
+ })
+ }
+
+ if (impl.is_equivalence) {
+ for (const assumption of assumptions) {
+ implications.push({
+ id: impl.id,
+ assumptions: new Set(conclusions),
+ source_assumptions: new Set(source_assumptions),
+ target_assumptions: new Set(target_assumptions),
+ conclusion: assumption,
+ relations,
+ })
+ }
+ }
+ }
+
+ return implications
+}
+
+async function get_functors(tx: Transaction) {
+ const res = await tx.execute(`
+ SELECT
+ id,
+ name,
+ source,
+ target,
+ (
+ SELECT json_group_array(property_id) FROM (
+ SELECT property_id
+ FROM category_property_assignments
+ WHERE category_id = source AND is_satisfied = TRUE
+ )
+ ) as source_props,
+ (
+ SELECT json_group_array(property_id) FROM (
+ SELECT property_id
+ FROM category_property_assignments
+ WHERE category_id = target AND is_satisfied = TRUE
+ )
+ ) as target_props
+ FROM functors
+ ORDER BY lower(name)
+ `)
+
+ return res.rows.map((row) => ({
+ id: row.id,
+ name: row.name,
+ source: row.source,
+ target: row.target,
+ source_props: new Set(JSON.parse(row.source_props as string)),
+ target_props: new Set(JSON.parse(row.target_props as string)),
+ })) as FunctorMeta[]
+}
+
+async function delete_deduced_functor_properties(tx: Transaction, functor: FunctorMeta) {
+ await tx.execute({
+ sql: `
+ DELETE FROM functor_property_assignments
+ WHERE functor_id = ? AND is_deduced = TRUE
+ `,
+ args: [functor.id],
+ })
+}
+
+async function deduce_satisfied_functor_properties(
+ tx: Transaction,
+ functor: FunctorMeta,
+ implications: NormalizedFunctorImplication[],
+) {
+ const satisfied_res = await tx.execute({
+ sql: `
+ SELECT property_id
+ FROM functor_property_assignments
+ WHERE
+ functor_id = ?
+ AND is_satisfied = TRUE
+ AND is_deduced = FALSE
+ `,
+ args: [functor.id],
+ })
+
+ const satisfied_props = new Set(
+ satisfied_res.rows.map((row) => row.property_id) as string[],
+ ) as Set
+
+ const deduced_satisfied_props: string[] = []
+ const reasons: Record = {}
+
+ while (true) {
+ const implication = implications.find(
+ ({ assumptions, conclusion, source_assumptions, target_assumptions }) =>
+ is_subset(assumptions, satisfied_props) &&
+ !satisfied_props.has(conclusion) &&
+ is_subset(source_assumptions, functor.source_props) &&
+ is_subset(target_assumptions, functor.target_props),
+ )
+ if (!implication) break
+
+ const { id: implication_id, conclusion } = implication
+
+ satisfied_props.add(conclusion)
+ deduced_satisfied_props.push(conclusion)
+
+ const assumption_string = get_assumption_string(implication)
+ const conclusion_string = get_conclusion_string(implication)
+
+ const ref = `(see here)`
+ const reason = `Since it ${assumption_string}, it ${conclusion_string} ${ref}.`
+
+ reasons[conclusion] = reason
+ }
+
+ if (deduced_satisfied_props.length > 0) {
+ const value_fragments: string[] = []
+ const values: (string | number)[] = []
+
+ for (let i = 0; i < deduced_satisfied_props.length; i++) {
+ const id = deduced_satisfied_props[i]
+ value_fragments.push(`(?, ?, TRUE, ?, ?, TRUE)`)
+ values.push(functor.id, id, reasons[id], i + 1)
+ }
+
+ const insert_sql = `
+ INSERT INTO functor_property_assignments (
+ functor_id, property_id, is_satisfied, reason, position, is_deduced
+ )
+ VALUES
+ ${value_fragments.join(',\n')}
+ `
+
+ await tx.execute({ sql: insert_sql, args: values })
+ }
+
+ console.info(
+ `Added ${deduced_satisfied_props.length} satisfied properties for functor ${functor.id} to the database`,
+ )
+}
+
+async function deduce_unsatisfied_functor_properties(
+ tx: Transaction,
+ functor: FunctorMeta,
+ implications: NormalizedFunctorImplication[],
+) {
+ const satisfied_res = await tx.execute({
+ sql: `
+ SELECT property_id
+ FROM functor_property_assignments
+ WHERE functor_id = ? AND is_satisfied = TRUE
+ `,
+ args: [functor.id],
+ })
+
+ const satisfied_props = new Set(
+ satisfied_res.rows.map((row) => row.property_id) as string[],
+ )
+
+ const unsatisfied_res = await tx.execute({
+ sql: `
+ SELECT property_id
+ FROM functor_property_assignments
+ WHERE
+ functor_id = ?
+ AND is_satisfied = FALSE
+ AND is_deduced = FALSE
+ `,
+ args: [functor.id],
+ })
+
+ const unsatisfied_props = new Set(
+ unsatisfied_res.rows.map((row) => row.property_id) as string[],
+ )
+
+ const deduced_unsatisfied_props: string[] = []
+ const reasons: Record = {}
+
+ function get_next_implication() {
+ for (const implication of implications) {
+ if (!unsatisfied_props.has(implication.conclusion)) continue
+ for (const p of implication.assumptions) {
+ const is_valid =
+ !unsatisfied_props.has(p) &&
+ is_subset(implication.assumptions, satisfied_props, p) &&
+ is_subset(implication.source_assumptions, functor.source_props) &&
+ is_subset(implication.target_assumptions, functor.target_props)
+
+ if (is_valid) return { implication, property: p }
+ }
+ }
+
+ return null
+ }
+
+ while (true) {
+ const next = get_next_implication()
+ if (!next) break
+
+ const { implication, property } = next
+ const { id: implication_id, relations } = implication
+
+ if (satisfied_props.has(property)) {
+ throw new Error(`Contradiction has been found for: ${property}`)
+ }
+
+ unsatisfied_props.add(property)
+ deduced_unsatisfied_props.push(property)
+
+ const assumption_string = get_assumption_string(implication)
+ const conclusion_string = get_conclusion_string(implication)
+
+ const ref = `(see here)`
+
+ const reason =
+ `Assume that it ${relations[property]} ${property}. ` +
+ `But since it ${assumption_string}, it ${conclusion_string} ${ref} – contradiction.`
+
+ reasons[property] = reason
+ }
+
+ if (deduced_unsatisfied_props.length > 0) {
+ const value_fragments: string[] = []
+ const values: (string | number)[] = []
+
+ for (let i = 0; i < deduced_unsatisfied_props.length; i++) {
+ const id = deduced_unsatisfied_props[i]
+ value_fragments.push('(?, ?, FALSE, ?, ?, TRUE)')
+ values.push(functor.id, id, reasons[id], i + 1)
+ }
+
+ const insert_query = `
+ INSERT INTO functor_property_assignments (
+ functor_id, property_id, is_satisfied, reason, position, is_deduced
+ )
+ VALUES
+ ${value_fragments.join(',\n')}`
+
+ await tx.execute({ sql: insert_query, args: values })
+ }
+
+ console.info(
+ `Added ${deduced_unsatisfied_props.length} unsatisfied properties for functor ${functor.id} to the database`,
+ )
+}
diff --git a/scripts/deduce.ts b/scripts/deduce.ts
index cc1b438d..df2618ac 100644
--- a/scripts/deduce.ts
+++ b/scripts/deduce.ts
@@ -1,7 +1,9 @@
import { createClient } from '@libsql/client'
import dotenv from 'dotenv'
-import { deduce_implications } from './deduce-implications'
-import { deduce_all_properties } from './deduce-properties'
+import { deduce_category_implications } from './deduce-category-implications'
+import { deduce_category_properties } from './deduce-category-properties'
+import { deduce_functor_implications } from './deduce-functor-implications'
+import { deduce_functor_properties } from './deduce-functor-properties'
dotenv.config({ quiet: true })
@@ -17,5 +19,8 @@ const db = createClient({
await db.execute('PRAGMA foreign_keys = ON')
-await deduce_implications(db)
-await deduce_all_properties(db)
+await deduce_category_implications(db)
+await deduce_category_properties(db)
+
+await deduce_functor_implications(db)
+await deduce_functor_properties(db)
diff --git a/scripts/implication.utils.ts b/scripts/implication.utils.ts
deleted file mode 100644
index c0430dc0..00000000
--- a/scripts/implication.utils.ts
+++ /dev/null
@@ -1,80 +0,0 @@
-import { Transaction } from '@libsql/client'
-
-export type NormalizedImplication = {
- id: string
- assumptions: Set
- conclusion: string
- relations: Record
-}
-
-export async function get_normalized_implications(
- tx: Transaction,
-): Promise {
- const res = await tx.execute(`
- SELECT
- v.id,
- v.assumptions,
- v.conclusions,
- v.is_equivalence,
- (
- SELECT json_group_object(p.id, p.relation)
- FROM properties p
- WHERE p.id IN (
- SELECT value FROM json_each(v.assumptions)
- UNION
- SELECT value FROM json_each(v.conclusions)
- )
- ) AS relations
- FROM implications_view v
- `)
-
- const all_implications_db = res.rows as unknown as {
- id: string
- assumptions: string
- conclusions: string
- is_equivalence: number
- relations: string
- }[]
-
- const implications: NormalizedImplication[] = []
-
- for (const impl of all_implications_db) {
- const assumptions: string[] = JSON.parse(impl.assumptions)
- const conclusions: string[] = JSON.parse(impl.conclusions)
- const relations: Record = JSON.parse(impl.relations)
-
- for (const conclusion of conclusions) {
- implications.push({
- id: impl.id,
- assumptions: new Set(assumptions),
- conclusion,
- relations,
- })
- }
-
- if (impl.is_equivalence) {
- for (const assumption of assumptions) {
- implications.push({
- id: impl.id,
- assumptions: new Set(conclusions),
- conclusion: assumption,
- relations,
- })
- }
- }
- }
-
- return implications
-}
-
-export function get_assumption_string(implication: NormalizedImplication): string {
- const { assumptions, relations } = implication
- return Array.from(assumptions)
- .map((assumption) => `${relations[assumption]} ${assumption}`)
- .join(' and ')
-}
-
-export function get_conclusion_string(implication: NormalizedImplication): string {
- const { conclusion, relations } = implication
- return `${relations[conclusion]} ${conclusion}`
-}
diff --git a/scripts/shared.ts b/scripts/shared.ts
new file mode 100644
index 00000000..883a13c1
--- /dev/null
+++ b/scripts/shared.ts
@@ -0,0 +1,36 @@
+export function are_equal_sets(a: Set, b: Set) {
+ return a.size === b.size && [...a].every((el) => b.has(el))
+}
+
+export function is_subset(a: Set, b: Set, exception?: T) {
+ for (const x of a) {
+ if (x !== exception && !b.has(x)) return false
+ }
+ return true
+}
+
+type NormalizedImplication = {
+ id: string
+ assumptions: Set
+ conclusion: string
+ relations: Record
+}
+
+export type NormalizedCategoryImplication = NormalizedImplication
+
+export type NormalizedFunctorImplication = NormalizedImplication & {
+ source_assumptions: Set
+ target_assumptions: Set
+}
+
+export function get_assumption_string(implication: NormalizedImplication): string {
+ const { assumptions, relations } = implication
+ return Array.from(assumptions)
+ .map((assumption) => `${relations[assumption]} ${assumption}`)
+ .join(' and ')
+}
+
+export function get_conclusion_string(implication: NormalizedImplication): string {
+ const { conclusion, relations } = implication
+ return `${relations[conclusion]} ${conclusion}`
+}
diff --git a/scripts/utils.ts b/scripts/utils.ts
deleted file mode 100644
index d7d3fe54..00000000
--- a/scripts/utils.ts
+++ /dev/null
@@ -1,3 +0,0 @@
-export function are_equal_sets(a: Set, b: Set) {
- return a.size === b.size && [...a].every((el) => b.has(el))
-}
diff --git a/src/components/FunctorImplicationItem.svelte b/src/components/FunctorImplicationItem.svelte
new file mode 100644
index 00000000..953a03d5
--- /dev/null
+++ b/src/components/FunctorImplicationItem.svelte
@@ -0,0 +1,87 @@
+
+
+
+
+
+
+{#each implication.assumptions as assumption, i}
+ {assumption}
+ {#if i < implication.assumptions.length - 1}
+
+ and
+ {/if}
+{/each}
+
+
+ {#if implication.is_equivalence}
+
+ {:else}
+
+ {/if}
+
+
+
+ {#if implication.is_equivalence}
+ is equivalent to
+ {:else}
+ implies
+ {/if}
+
+
+{#each implication.conclusions as conclusion, i}
+ {conclusion}
+ {#if i < implication.conclusions.length - 1}
+
+ and
+ {/if}
+{/each}
+{#if implication.source_assumptions.length > 0 || implication.target_assumptions.length > 0}
+ *
+{/if}
+
+
diff --git a/src/components/FunctorImplicationList.svelte b/src/components/FunctorImplicationList.svelte
new file mode 100644
index 00000000..fcdc5eb1
--- /dev/null
+++ b/src/components/FunctorImplicationList.svelte
@@ -0,0 +1,29 @@
+
+
+{#if implications.length}
+
+ {#each implications as implication}
+
+
+
+ {/each}
+
+
+
+ *Those implications also require assumptions on the source or target category.
+