diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index c5b6dabae..bf47b9444 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -56,7 +56,7 @@ You need to have [Git](https://git-scm.com/), [NodeJS](https://nodejs.org/) and ### Updating the Database -All updates to the database are made by modifying the YAML files in the folder [/databases/catdat/data](databases/catdat/data). See [DATABASE.md](/DATABASE.md) for an overview of the database structure. +All updates to the database are made by modifying the YAML files in the folder [/databases/catdat/data](databases/catdat/data). See [DATABASE.md](/DATABASE.md) for an overview of the database structure, and see [below](#authoring-of-yaml-files) for some tips how to edit YAML files. Apply the updates using: @@ -83,8 +83,8 @@ The `pnpm db:test` command runs several tests to ensure the data behaves as expe 1. Properties and their duals are mutual. 2. Categories and their duals are mutual. -3. For a specified list of categories (see [decided-categories.json](/databases/catdat/scripts/expected-data/decided-categories.json)), all properties have been decided. -4. Every property of the categories `Set`, `Ab`, `Top` matches precisely the expected properties defined in the [/databases/catdat/scripts/expected-data](/databases/catdat/scripts/expected-data/) folder. +3. For a specified list of categories (see [decided-categories.json](/databases/catdat/scripts/expected-data/decided-categories.json)) and functors (see [decided-functors.json](/databases/catdat/scripts/expected-data/decided-functors.json)), all properties have been decided. +4. Every property of the categories `Set`, `Ab`, `Top` and the functors `forget_vector`, `id_Set` matches precisely the expected properties defined in the [/databases/catdat/scripts/expected-data](/databases/catdat/scripts/expected-data/) folder. If any of these tests fail, adjust the data accordingly. @@ -102,33 +102,33 @@ 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. -- **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. +- **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 by a direct proof, 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). - **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). +- **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, regular monomorphisms, regular epimorphisms). -- **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 via some implication. Use the property detail page to check unknown categories. These proofs may also refer to other categories, in which case you may add links to their corresponding pages. As mentioned in the section on tests, for a list of selected categories it is actually mandatory to decide their properties. +- **Proofs for New Properties**: For every new property of categories (resp. functors), for each existing category (resp. functor), try to find a proof for whether it has this property or not, in case this has not already been deduced automatically via some implication. Use the property detail page to check unknown cases. These proofs may also refer to other categories (resp. functors), in which case you may add links to their corresponding pages. As mentioned in the section on tests, for a list of selected categories and functors it is actually mandatory to decide their properties. -- **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. +- **Counterexamples**: For any added property of categories, ensure that at least one category does not satisfy it. If no existing category fits, add a new category that does not have the new property. The same remarks apply to properties of functors. -- **Easy properties first**: The order in which properties are assigned to a category will also be shown on its page. For this reason, prefer an order in which the trivial and easy assignments appear first. More technical properties should usually appear later. Assignments of closely related properties should also be grouped together whenever possible. +- **Easy properties first**: The order in which properties are assigned to a category (resp. functor) will also be shown on its page. For this reason, prefer an order in which the trivial and easy assignments appear first. More technical properties should usually appear later. Assignments of closely related properties should also be grouped together whenever possible. - **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. 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). -- **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. +- **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 combined automatically. - **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". When an implication can be phrased both in a "limit" or "colimit" variant, prefer the "limit" variant (unless the literature focusses on the "colimit" variant). - **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. +- **Simplify Implications**: When adding a new implication, check if it simplifies existing implications and if it deduces some previously non-deduced properties. -- **Long-form content**: If a proof for a property becomes very long, move it into a markdown-generated content page and link to that page. These files are located in the `/content` folder. For example, `/content/cocongruences_of_groups.md` is rendered at [`/content/cocongruences_of_groups`](https://catdat.app/content/cocongruences_of_groups). Content pages are also used for reusable lemmas that apply to multiple property assignments. +- **Long-form content**: If a proof for a property becomes very long, move it into a markdown-generated content page and link to that page. These files are located in the [`/content`](/content/) folder. For example, `/content/cocongruences_of_groups.md` is rendered at [`/content/cocongruences_of_groups`](https://catdat.app/content/cocongruences_of_groups). Content pages are also used for reusable lemmas that apply to multiple property assignments. - **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. @@ -150,7 +150,7 @@ In particular, it often makes sense to **keep** a redundant assignment of a sati 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.yaml` for an example. +Every redundant assignment of a satisfied property that is intentionally kept must be explicitly marked to skip the redundancy check. See [`N.yaml`](/databases/catdat/data/categories/N.yaml) for an example. ### Keep Pull Requests Focused @@ -181,9 +181,9 @@ AI tools may be used to assist with development in this repository, but not to r - Use AI to support your workflow (e.g. by asking questions, getting suggestions, or creating snippets), not to generate complete features or large portions of code without your active involvement. - AI agents that autonomously generate or modify code are not allowed. Pull requests that are mainly written by AI agents will be closed. -- AI can also be used to find proofs for properties of categories, but they must be checked thoroughly and written in your own words. +- AI can also be used to find proofs for properties of categories and functors, but they must be checked thoroughly and written in your own words. - AI may also be used to improve English writing (e.g. grammar, clarity, phrasing), particularly if you are not a native speaker. -- Every line of code in a pull request must be understood by the developer submitting it. +- Every line of code in a pull request must be understood by the person submitting it. - Pull request descriptions and commit messages must be written manually. AI-generated summaries are often superficial, meaningless, and do not tell the whole story. In summary, treat AI as a productivity tool, not as a substitute for understanding or authorship. @@ -194,6 +194,6 @@ If you are not familiar with YAML, a short beginner-friendly introduction can be 1. It is recommended to enable word wrap in your editor when working with YAML files. 2. HTML may be used inside string values, for example for links (``), italic text (``), and ordered lists (`
    `). -3. Use single-quoted strings (`'...'`) for values containing `:`. See `Cat.yaml` for an example. Inside single-quoted strings, a literal single quote must be escaped as `''`. See `Man.yaml` for an example. -4. Use `>-` for multiline text that should be rendered as a single paragraph without line breaks. This is particularly useful for improving readability of longer texts or HTML lists in the YAML file itself. See `core-thin.yaml` for an example. -5. Use `|-` for multiline text where line breaks should be preserved. These line breaks are automatically converted to `
    ` when rendered. See `FreeAb.yaml` for an example. +3. Use single-quoted strings (`'...'`) for values containing `:`. See [`Cat.yaml`](/databases/catdat/data/categories/Cat.yaml) for an example. Inside single-quoted strings, a literal single quote must be escaped as `''`. See [`Man.yaml`](/databases/catdat/data/categories/Man.yaml) for an example. +4. Use `>-` for multiline text that should be rendered as a single paragraph without line breaks. This is particularly useful for improving readability of longer texts or HTML lists in the YAML file itself. See [`core-thin.yaml`](/databases/catdat/data/category-properties/core-thin.yaml) for an example. +5. Use `|-` for multiline text where line breaks should be preserved. These line breaks are automatically converted to `
    ` when rendered. See [`FreeAb.yaml`](/databases/catdat/data/categories/FreeAb.yaml) for an example. diff --git a/DATABASE.md b/DATABASE.md index 54c79b8fe..f8da422ea 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -4,74 +4,113 @@ _CatDat_ is based on a [SQLite database](https://sqlite.org/). During runtime of the application, it is read-only. -The local copy of the database is located at `/databases/catdat/catdat.db`. It has three main tables: +The local copy of the database is located at `/databases/catdat/catdat.db`. It contains three main tables: + +- `structures` +- `properties` +- `implications` + +The `structures` table stores data that is common to all types of categorical structures. Two types are currently supported: categories and functors. They are stored in the following table: + +- `structure_types` + +Structure-specific data is stored in additional tables, such as: - `categories` -- `category_properties` -- `category_implications` +- `functors` -To associate properties with categories (satisfied or not), there is a table: +Properties (whether satisfied or not) are associated with categorical structures via the following table: -- `category_property_assignments` +- `property_assignments` To mark properties as assumptions or conclusions of an implication, there are two tables: -- `category_implication_assumptions` -- `category_implication_conclusions` +- `assumptions` +- `conclusions` -But they are abstracted away by using the view `category_implications_view`. +These tables are abstracted through the `implications_view` view. -Further tables are: +Functor implications may also depend on properties of the source or target category. Such dependencies are stored in the table: -- `category_tags` -- `category_tag_assignments` -- `related_categories` -- `relations` -- `special_object_types` -- `special_objects` -- `special_morphism_types` -- `special_morphisms` -- `related_category_properties` -- `category_comments` +- `mapped_assumptions` -For functors there are similar tables, such as: - -- `functors` -- `functor_properties` -- `functor_implications` -- `functor_property_assignments` +Additional tables are available. For a complete overview, see the diagram below. ## Schema vs. Data -The schema defines the structure of the database: tables, views, indexes, and triggers. It is specified in several SQL files located in the subfolder [/databases/catdat/schema](/databases/catdat/schema/). The command `pnpm db:setup` deletes the old database file (if it exists) and creates a new one using this schema. This is required when the schema changes, so it is recommended to run it periodically. +The schema defines the structure of the database: tables, views, indexes, and triggers. It is specified in several SQL files located in the subfolder [/databases/catdat/schema](/databases/catdat/schema/). The command + +``` +pnpm db:setup +``` + +deletes the old database file (if it exists) and creates a new one using this schema. This is required when the schema changes. + +Database entries (categories, functors, properties, implications, etc.) are defined in YAML files located in the subfolder [/databases/catdat/data](/databases/catdat/data/). The command + +``` +pnpm db:seed +``` -Database entries (categories, properties, implications, etc.) are defined in YAML files located in the subfolder [/databases/catdat/data](/databases/catdat/data/). The command `pnpm db:seed` rebuilds the database by clearing all existing data and then parsing and inserting the entries defined in these YAML files. +rebuilds the database by clearing all existing data and then parsing and inserting the entries defined in these YAML files. ## Derived Data -From the defined satisfied properties of a given category, new properties can be automatically deduced using the implications. (For example, when a category has equalizers and products, we can infer that it is complete.) The same applies to unsatisfied properties. Additionally, suitable implications may be dualized, and a category inherits all dualized properties of its dual category, if available. Note that the YAML files mentioned above do _not_ contain any derived data. +From the defined satisfied properties of a given categorical structure, new properties can be automatically deduced using the implications. (For example, when a category has equalizers and products, we can infer that it is complete.) The same applies to unsatisfied properties. -The command `pnpm db:deduce` deduces implications, satisfied properties, and unsatisfied properties. +Additionally, suitable implications may be dualized, and a categorical structure inherits all dualized properties of its dual structure, if available. Note that the YAML files mentioned above do _not_ contain any derived data. + +The command + +``` +pnpm db:deduce +``` + +deduces implications, satisfied properties, and unsatisfied properties. ## Test Data -The command `pnpm db:test` executes some tests and verifies that the data behaves as expected. +The command + +``` +pnpm db:test +``` + +executes some tests and verifies that the data behaves as expected. ## One command for everything -Use `pnpm db:update` to run all the commands in sequence: `pnpm db:seed`,`pnpm db:deduce`, and `pnpm db:test`. +Use the command + +``` +pnpm db:update +``` -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. +to run all the commands in sequence: `pnpm db:seed`,`pnpm db:deduce`, and `pnpm db:test`. This also creates a copy of the local database in the `/static` folder. + +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 to categories. +There is another script that intentionally does not run with each update. Use the command + +``` +pnpm db:redundancies +``` + +to check for redundant assignments of properties to categorical structures. ## Diagram -This is the database schema as of 26.05.2026; changes may occur. +This is the database schema as of 16.06.2026; changes may occur. -database diagram +database diagram ## Application Database diff --git a/DEPLOYMENT.md b/DEPLOYMENT.md index 25ac196df..0188373be 100644 --- a/DEPLOYMENT.md +++ b/DEPLOYMENT.md @@ -7,7 +7,7 @@ This page is only relevant to the maintainer(s) of this project. ## Prerendering -Most pages are prerendered for performance reasons. This implies that the database is consumed at build time to generate static HTML pages. The only non-prerendered pages are the search and comparison pages, since they involve dynamic lists of properties and categories. +Most pages are prerendered for performance reasons. This implies that the database is consumed at build time to generate static HTML pages. The only non-prerendered pages are the search and comparison pages, since they involve dynamic lists of properties and categories resp. functors. ## Databases diff --git a/README.md b/README.md index 6be1edc96..6fecf5d9e 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ and properties. Built by and for those who love [category theory](https://en.wik - **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 and functors based on satisfied properties and unsatisfied properties. -- **Comparison Feature**: Compare multiple categories to identify their differences and similarities. +- **Comparison Feature**: Compare multiple categories and functors 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/databases/catdat/data/functor-implications/adjoints.yaml b/databases/catdat/data/functor-implications/adjoints.yaml index d1b8ebbbe..abd14f5b7 100644 --- a/databases/catdat/data/functor-implications/adjoints.yaml +++ b/databases/catdat/data/functor-implications/adjoints.yaml @@ -1,8 +1,6 @@ - id: right_adjoint_consequences assumptions: - right adjoint - source_assumptions: [] - target_assumptions: [] conclusions: - continuous proof: This is standard, see     Mac Lane, Ch. V, Theorem 5.1. @@ -11,13 +9,14 @@ - id: saft assumptions: - continuous - source_assumptions: - - cogenerating set - - complete - - locally small - - well-powered - target_assumptions: - - locally small + mapped_assumptions: + source: + - cogenerating set + - complete + - locally small + - well-powered + target: + - locally small conclusions: - right adjoint proof: 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. diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml index d504ef34e..c9f1916ad 100644 --- a/databases/catdat/data/functor-implications/equivalences.yaml +++ b/databases/catdat/data/functor-implications/equivalences.yaml @@ -3,8 +3,6 @@ - essentially surjective - faithful - full - source_assumptions: [] - target_assumptions: [] conclusions: - equivalence proof: This is standard, see Mac Lane, Ch. IV, Theorem 4.1. @@ -13,8 +11,6 @@ - id: equivalence_consequences assumptions: - equivalence - source_assumptions: [] - target_assumptions: [] conclusions: - monadic - left-invertible diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml index 63bf1d376..ee9b91ead 100644 --- a/databases/catdat/data/functor-implications/limits preservation.yaml +++ b/databases/catdat/data/functor-implications/limits preservation.yaml @@ -1,8 +1,6 @@ - id: continuous_consequences assumptions: - continuous - source_assumptions: [] - target_assumptions: [] conclusions: - cofinitary - preserves products @@ -13,8 +11,6 @@ - id: products_consequences assumptions: - preserves products - source_assumptions: [] - target_assumptions: [] conclusions: - preserves finite products proof: This is trivial. @@ -23,8 +19,6 @@ - id: finite_products_consequences assumptions: - preserves finite products - source_assumptions: [] - target_assumptions: [] conclusions: - preserves terminal objects proof: This is trivial. @@ -34,9 +28,9 @@ assumptions: - preserves equalizers - preserves products - source_assumptions: - - products - target_assumptions: [] + mapped_assumptions: + source: + - products conclusions: - continuous proof: This follows from the construction of limits via equalizers and products, see Mac Lane, Ch. V, Theorem 2.2. @@ -46,9 +40,9 @@ assumptions: - cofinitary - left exact - source_assumptions: - - finitely complete - target_assumptions: [] + mapped_assumptions: + source: + - finitely complete conclusions: - continuous proof: This is because every limit can be written as a filtered limit of finite limits, see Mac Lane, Ch. IX, Theorem 1.1. @@ -58,9 +52,9 @@ assumptions: - cofinitary - preserves finite products - source_assumptions: - - finite products - target_assumptions: [] + mapped_assumptions: + source: + - finite products conclusions: - preserves products proof: This is because every product can be written as a filtered limit of finite products, see Mac Lane, Ch. IX, Theorem 1.1. @@ -69,8 +63,6 @@ - id: exact_definition assumptions: - exact - source_assumptions: [] - target_assumptions: [] conclusions: - left exact - right exact @@ -80,8 +72,6 @@ - id: left_exact_consequences assumptions: - left exact - source_assumptions: [] - target_assumptions: [] conclusions: - preserves finite products - preserves equalizers @@ -96,9 +86,9 @@ assumptions: - preserves equalizers - preserves finite products - source_assumptions: - - finite products - target_assumptions: [] + mapped_assumptions: + source: + - finite products conclusions: - left exact proof: This follows from the construction of finite limits via equalizers and finite products, see Mac Lane, Ch. V, Theorem 2.2. @@ -107,8 +97,6 @@ - id: representable_is_continuous assumptions: - representable - source_assumptions: [] - target_assumptions: [] conclusions: - continuous proof: This is standard, see Mac Lane, Ch. V, Theorem 4.1. @@ -117,8 +105,6 @@ - id: equalizers_include_coreflexive_equalizers assumptions: - preserves equalizers - source_assumptions: [] - target_assumptions: [] conclusions: - preserves coreflexive equalizers proof: This is trivial. @@ -128,9 +114,9 @@ assumptions: - preserves coreflexive equalizers - preserves finite products # TODO: only need binary products - source_assumptions: - - binary products - target_assumptions: [] + mapped_assumptions: + source: + - binary products conclusions: - preserves equalizers proof: This follows easily from this result about categories. @@ -139,9 +125,9 @@ - id: mono-preserving_criterion assumptions: - preserves equalizers - source_assumptions: - - mono-regular - target_assumptions: [] + mapped_assumptions: + source: + - mono-regular conclusions: - preserves monomorphisms proof: Any monomorphism in the domain is a regular monomorphism and is mapped to a regular monomorphism. diff --git a/databases/catdat/data/functor-implications/misc.yaml b/databases/catdat/data/functor-implications/misc.yaml index 068a10ea0..bed2217cc 100644 --- a/databases/catdat/data/functor-implications/misc.yaml +++ b/databases/catdat/data/functor-implications/misc.yaml @@ -2,9 +2,9 @@ assumptions: - conservative - preserves equalizers - source_assumptions: - - equalizers - target_assumptions: [] + mapped_assumptions: + source: + - equalizers conclusions: - faithful proof: '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$.' @@ -14,8 +14,6 @@ assumptions: - full - faithful - source_assumptions: [] - target_assumptions: [] conclusions: - conservative proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$. @@ -27,8 +25,6 @@ - conservative conclusions: - essentially injective - source_assumptions: [] - target_assumptions: [] proof: 'The functor even lifts isomorphisms: If $F(A) \to F(B)$ is an isomorphism, then it is induced by a morphism $A \to B$ since $F$ is full. Moreover, $A \to B$ is an isomorphism since its $F$-image is an isomorphism and $F$ is conservative.' is_equivalence: false @@ -39,7 +35,5 @@ - faithful - essentially injective - conservative - source_assumptions: [] - target_assumptions: [] proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is am morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.' is_equivalence: false diff --git a/databases/catdat/data/functor-implications/monadic.yaml b/databases/catdat/data/functor-implications/monadic.yaml index b5672a55b..e10fe05e2 100644 --- a/databases/catdat/data/functor-implications/monadic.yaml +++ b/databases/catdat/data/functor-implications/monadic.yaml @@ -1,8 +1,6 @@ - id: monadic_consequences assumptions: - monadic - source_assumptions: [] - target_assumptions: [] conclusions: - conservative - faithful @@ -15,9 +13,9 @@ - right adjoint - conservative - preserves reflexive coequalizers - source_assumptions: - - reflexive coequalizers - target_assumptions: [] + mapped_assumptions: + source: + - reflexive coequalizers conclusions: - monadic proof: This is the crude monadicity theorem. A proof can be found in Mac Lane & Moerdijk, Thm. IV.4.2. diff --git a/databases/catdat/data/functor-properties/representable.yaml b/databases/catdat/data/functor-properties/representable.yaml index 8d3ae7480..bec89ed04 100644 --- a/databases/catdat/data/functor-properties/representable.yaml +++ b/databases/catdat/data/functor-properties/representable.yaml @@ -1,7 +1,6 @@ id: representable relation: is description: 'A functor $F : \C \to \D$ is representable if $\C$ is locally small, $\D = \Set$, and there is an object $A \in \C$ with $F \cong \Hom(A,-)$.' -required_target: Set nlab_link: https://ncatlab.org/nlab/show/representable+functor invariant_under_equivalences: true dual_property: null diff --git a/databases/catdat/schema/001_structures.sql b/databases/catdat/schema/001_structures.sql new file mode 100644 index 000000000..ed89d1bff --- /dev/null +++ b/databases/catdat/schema/001_structures.sql @@ -0,0 +1,76 @@ +CREATE TABLE structure_types ( + type TEXT PRIMARY KEY +); + +INSERT INTO structure_types (type) VALUES + ('category'), + ('functor'); + +CREATE TABLE structures ( + id TEXT PRIMARY KEY, + type TEXT NOT NULL, + name TEXT NOT NULL UNIQUE, + notation TEXT NOT NULL, + description TEXT, + nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), + dual_structure_id TEXT, + UNIQUE (id, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, + FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT +); + +CREATE UNIQUE INDEX structures_lower_id_unique ON structures (lower(id)); + +CREATE INDEX structure_by_type ON structures (type); + +CREATE TABLE related_structures ( + structure_id TEXT NOT NULL, + related_structure_id TEXT NOT NULL, + type TEXT NOT NULL, + CHECK (structure_id != related_structure_id), + PRIMARY KEY (structure_id, related_structure_id), + FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (related_structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE +); + +CREATE TABLE structure_comments ( + id INTEGER PRIMARY KEY, + structure_id TEXT NOT NULL, + comment TEXT NOT NULL, + FOREIGN KEY (structure_id) REFERENCES structures (id) ON DELETE CASCADE +); + +CREATE INDEX idx_structure_comments ON structure_comments (structure_id); + +CREATE TABLE tags ( + id INTEGER PRIMARY KEY, + tag TEXT NOT NULL, + type TEXT NOT NULL, + UNIQUE (tag, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT +); + +CREATE TABLE structure_tag_assignments ( + structure_id TEXT NOT NULL, + type TEXT NOT NULL, + tag TEXT NOT NULL, + PRIMARY KEY (structure_id, type, tag), + FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (tag, type) REFERENCES tags (tag, type) ON DELETE CASCADE +); + +CREATE TABLE structure_maps ( + map TEXT NOT NULL, + type TEXT NOT NULL, + mapped_type TEXT NOT NULL, + PRIMARY KEY (map, type, mapped_type), + UNIQUE (map, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, + FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE +); + +INSERT INTO structure_maps + (map, type, mapped_type) +VALUES + ('source', 'functor', 'category'), + ('target', 'functor', 'category'); \ No newline at end of file diff --git a/databases/catdat/schema/001_tags.sql b/databases/catdat/schema/001_tags.sql deleted file mode 100644 index 544a385d4..000000000 --- a/databases/catdat/schema/001_tags.sql +++ /dev/null @@ -1,9 +0,0 @@ -CREATE TABLE category_tags ( - id INTEGER PRIMARY KEY, - tag TEXT NOT NULL UNIQUE -); - -CREATE TABLE functor_tags ( - id INTEGER PRIMARY KEY, - tag TEXT NOT NULL UNIQUE -); \ No newline at end of file diff --git a/databases/catdat/schema/002_properties.sql b/databases/catdat/schema/002_properties.sql new file mode 100644 index 000000000..72b995f84 --- /dev/null +++ b/databases/catdat/schema/002_properties.sql @@ -0,0 +1,55 @@ +CREATE TABLE relations ( + relation TEXT PRIMARY KEY, + conditional TEXT NOT NULL +); + +CREATE TABLE properties ( + id TEXT PRIMARY KEY, + type TEXT NOT NULL, + 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, + UNIQUE (id, type), -- TODO: make (id, type) the primary key + FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT, + FOREIGN KEY (dual_property_id, type) + REFERENCES properties (id, type) ON DELETE RESTRICT, + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT +); + +CREATE UNIQUE INDEX properties_lower_id_unique ON properties (lower(id)); + +CREATE TABLE related_properties ( + property_id TEXT NOT NULL, + related_property_id TEXT NOT NULL, + type TEXT NOT NULL, + CHECK (property_id != related_property_id), + PRIMARY KEY (property_id, related_property_id), + FOREIGN KEY (property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE, + FOREIGN KEY (related_property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE TABLE property_assignments ( + id INTEGER PRIMARY KEY, + structure_id TEXT NOT NULL, + property_id TEXT NOT NULL, + type TEXT NOT NULL, + is_satisfied INTEGER + -- we use NULL for undecidable properties + CHECK (is_satisfied in (TRUE, FALSE, NULL)), + proof TEXT NOT NULL CHECK (length(proof) > 0), + is_deduced INTEGER NOT NULL DEFAULT FALSE + CHECK (is_deduced in (TRUE, FALSE)), + check_redundancy INTEGER NOT NULL DEFAULT TRUE + CHECK (check_redundancy in (TRUE, FALSE)), + UNIQUE (structure_id, property_id), + FOREIGN KEY (structure_id, type) + REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE INDEX idx_property_assigned ON property_assignments (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/002_relations.sql b/databases/catdat/schema/002_relations.sql deleted file mode 100644 index e49f47097..000000000 --- a/databases/catdat/schema/002_relations.sql +++ /dev/null @@ -1,4 +0,0 @@ -CREATE TABLE relations ( - relation TEXT PRIMARY KEY, - conditional TEXT NOT NULL -); \ No newline at end of file diff --git a/databases/catdat/schema/003_categories.sql b/databases/catdat/schema/003_categories.sql deleted file mode 100644 index 87ec2192d..000000000 --- a/databases/catdat/schema/003_categories.sql +++ /dev/null @@ -1,39 +0,0 @@ -CREATE TABLE categories ( - id TEXT PRIMARY KEY, - name TEXT NOT NULL UNIQUE, - notation TEXT NOT NULL, - objects TEXT NOT NULL, - morphisms TEXT NOT NULL, - description TEXT, - nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), - dual_category_id TEXT REFERENCES categories (id) -); - -CREATE UNIQUE INDEX categories_lower_id_unique ON categories (lower(id)); - -CREATE TABLE category_tag_assignments ( - category_id TEXT NOT NULL, - tag TEXT NOT NULL, - PRIMARY KEY (category_id, tag), - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (tag) REFERENCES category_tags (tag) ON DELETE CASCADE -); - -CREATE TABLE related_categories ( - category_id TEXT NOT NULL, - related_category_id TEXT NOT NULL, - PRIMARY KEY (category_id, related_category_id), - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (related_category_id) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE TABLE category_comments ( - id INTEGER PRIMARY KEY, - category_id TEXT NOT NULL, - comment TEXT NOT NULL, - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE INDEX idx_category_comments ON category_comments (category_id); - - diff --git a/databases/catdat/schema/003_implications.sql b/databases/catdat/schema/003_implications.sql new file mode 100644 index 000000000..ea54f76c7 --- /dev/null +++ b/databases/catdat/schema/003_implications.sql @@ -0,0 +1,92 @@ +CREATE TABLE implications ( + id TEXT PRIMARY KEY, + type TEXT NOT NULL, + proof TEXT NOT NULL CHECK (length(proof) > 0), + is_equivalence INTEGER NOT NULL DEFAULT FALSE, + is_deduced INTEGER NOT NULL DEFAULT FALSE, + dualized_from TEXT, + UNIQUE (id, type), + CHECK (dualized_from IS NULL OR is_deduced = TRUE), + FOREIGN KEY (dualized_from, type) REFERENCES implications (id, type) ON DELETE RESTRICT, + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT +); + +CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id)); + +CREATE INDEX idx_implications_by_type ON implications (type); + +CREATE TABLE assumptions ( + implication_id TEXT NOT NULL, + property_id TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (implication_id, property_id), + FOREIGN KEY (implication_id, type) + REFERENCES implications (id, type) ON DELETE CASCADE, + FOREIGN KEY (property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE INDEX idx_assumptions_property ON assumptions (property_id); + +CREATE TABLE conclusions ( + implication_id TEXT NOT NULL, + property_id TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (implication_id, property_id), + FOREIGN KEY (implication_id, type) + REFERENCES implications (id, type) ON DELETE CASCADE, + FOREIGN KEY (property_id, type) + REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE INDEX idx_conclusions_property ON conclusions (property_id); + +CREATE TABLE mapped_assumptions ( + implication_id TEXT NOT NULL, + map TEXT NOT NULL, + property_id TEXT NOT NULL, + type TEXT NOT NULL, + property_type TEXT NOT NULL, + PRIMARY KEY (implication_id, map, property_id), + FOREIGN KEY (implication_id, type) + REFERENCES implications (id, type) ON DELETE CASCADE, + FOREIGN KEY (property_id, property_type) + REFERENCES properties (id, type) ON DELETE CASCADE, + FOREIGN KEY (map, type, property_type) + REFERENCES structure_maps (map, type, mapped_type) + ON DELETE RESTRICT +); + +CREATE INDEX idx_assumptions_mapped_property ON mapped_assumptions (property_id); + +CREATE VIEW implications_view AS + SELECT + i.id, + i.type, + i.is_equivalence, + i.is_deduced, + i.dualized_from, + i.proof, + ( + SELECT json_group_array(a.property_id) + FROM assumptions a WHERE a.implication_id = i.id + ORDER BY lower(a.property_id) + ) AS assumptions, + ( + SELECT json_group_array(c.property_id) + FROM conclusions c WHERE c.implication_id = i.id + ORDER BY lower(c.property_id) + ) AS conclusions, + ( + SELECT json_group_object(map, properties) + FROM ( + SELECT + a.map, + json_group_array(a.property_id) AS properties + FROM mapped_assumptions a + WHERE a.implication_id = i.id + GROUP BY a.map + ) + ) AS mapped_assumptions + FROM implications i +; \ No newline at end of file diff --git a/databases/catdat/schema/004_categories.sql b/databases/catdat/schema/004_categories.sql new file mode 100644 index 000000000..1e357aab0 --- /dev/null +++ b/databases/catdat/schema/004_categories.sql @@ -0,0 +1,17 @@ +CREATE TABLE categories ( + id TEXT PRIMARY KEY, + objects TEXT NOT NULL, + morphisms TEXT NOT NULL, + FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE +); + +CREATE TRIGGER trg_category_type_check +BEFORE INSERT ON categories +BEGIN + SELECT + CASE + WHEN + (SELECT type FROM structures WHERE id = NEW.id) != 'category' + THEN RAISE(ABORT, 'Categories must have type "category"') + END; +END; \ No newline at end of file diff --git a/databases/catdat/schema/004_category-properties.sql b/databases/catdat/schema/004_category-properties.sql deleted file mode 100644 index 9604ad826..000000000 --- a/databases/catdat/schema/004_category-properties.sql +++ /dev/null @@ -1,39 +0,0 @@ -CREATE TABLE category_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 category_properties (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX category_properties_lower_id_unique ON category_properties (lower(id)); - -CREATE TABLE related_category_properties ( - property_id TEXT NOT NULL, - related_property_id TEXT NOT NULL, - PRIMARY KEY (property_id, related_property_id), - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE, - FOREIGN KEY (related_property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE TABLE category_property_assignments ( - id INTEGER PRIMARY KEY, - category_id TEXT NOT NULL, - property_id TEXT NOT NULL, - is_satisfied INTEGER - -- we use NULL for undecidable properties - CHECK (is_satisfied in (TRUE, FALSE, NULL)), - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_deduced INTEGER NOT NULL DEFAULT FALSE - CHECK (is_deduced in (TRUE, FALSE)), - check_redundancy INTEGER NOT NULL DEFAULT TRUE - CHECK (check_redundancy in (TRUE, FALSE)), - UNIQUE (category_id, property_id), - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE INDEX idx_property_category ON category_property_assignments (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/005_category-implications.sql b/databases/catdat/schema/005_category-implications.sql deleted file mode 100644 index 52d81ea07..000000000 --- a/databases/catdat/schema/005_category-implications.sql +++ /dev/null @@ -1,31 +0,0 @@ -CREATE TABLE category_implications ( - id TEXT PRIMARY KEY, - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_equivalence INTEGER NOT NULL DEFAULT FALSE, - is_deduced INTEGER NOT NULL DEFAULT FALSE, - dualized_from TEXT, - CHECK (dualized_from IS NULL OR is_deduced = TRUE), - FOREIGN KEY (dualized_from) REFERENCES category_implications (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX category_implications_lower_id_unique ON category_implications (lower(id)); - -CREATE TABLE category_implication_assumptions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES category_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE TABLE category_implication_conclusions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES category_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE INDEX idx_assumptions_category_property ON category_implication_assumptions (property_id); - -CREATE INDEX idx_conclusions_category_property ON category_implication_conclusions (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/007_special_objects.sql b/databases/catdat/schema/005_special_objects.sql similarity index 100% rename from databases/catdat/schema/007_special_objects.sql rename to databases/catdat/schema/005_special_objects.sql diff --git a/databases/catdat/schema/006_category-implications-view.sql b/databases/catdat/schema/006_category-implications-view.sql deleted file mode 100644 index 7f60eb259..000000000 --- a/databases/catdat/schema/006_category-implications-view.sql +++ /dev/null @@ -1,47 +0,0 @@ -CREATE VIEW category_implications_view AS -SELECT - i.id, - i.is_equivalence, - i.proof, - i.is_deduced, - i.dualized_from, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_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 category_implication_conclusions c - WHERE c.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS conclusions -FROM category_implications i; - - -CREATE TRIGGER trg_category_implications_view_insert -INSTEAD OF INSERT ON category_implications_view -BEGIN - INSERT INTO category_implications - (id, is_equivalence, proof, is_deduced, dualized_from) - VALUES ( - NEW.id, - COALESCE(NEW.is_equivalence, FALSE), - NEW.proof, - COALESCE(NEW.is_deduced, FALSE), - NEW.dualized_from - ); - - INSERT INTO category_implication_assumptions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.assumptions); - - INSERT INTO category_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/databases/catdat/schema/008_special-morphisms.sql b/databases/catdat/schema/006_special-morphisms.sql similarity index 100% rename from databases/catdat/schema/008_special-morphisms.sql rename to databases/catdat/schema/006_special-morphisms.sql diff --git a/databases/catdat/schema/007_functors.sql b/databases/catdat/schema/007_functors.sql new file mode 100644 index 000000000..a1982c617 --- /dev/null +++ b/databases/catdat/schema/007_functors.sql @@ -0,0 +1,24 @@ +CREATE TABLE functors ( + id TEXT PRIMARY KEY, + source TEXT NOT NULL, + target TEXT NOT NULL, + left_adjoint TEXT, + UNIQUE (id, source, target), + FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, + FOREIGN KEY (source) REFERENCES categories (id) ON DELETE CASCADE, + FOREIGN KEY (target) REFERENCES categories (id) ON DELETE CASCADE, + FOREIGN KEY (left_adjoint, target, source) + REFERENCES functors (id, source, target) + ON DELETE CASCADE +); + +CREATE TRIGGER trg_functor_type_check +BEFORE INSERT ON functors +BEGIN + SELECT + CASE + WHEN + (SELECT type FROM structures WHERE id = NEW.id) != 'functor' + THEN RAISE(ABORT, 'Functors must have type "functor"') + END; +END; \ No newline at end of file diff --git a/databases/catdat/schema/009_functors.sql b/databases/catdat/schema/009_functors.sql deleted file mode 100644 index 418c3b6ff..000000000 --- a/databases/catdat/schema/009_functors.sql +++ /dev/null @@ -1,38 +0,0 @@ -CREATE TABLE functors ( - id TEXT PRIMARY KEY, - name TEXT NOT NULL UNIQUE, - notation TEXT NOT NULL, - 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 -); - -CREATE UNIQUE INDEX functors_lower_id_unique ON functors (lower(id)); - -CREATE TABLE functor_tag_assignments ( - functor_id TEXT NOT NULL, - tag TEXT NOT NULL, - PRIMARY KEY (functor_id, tag), - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (tag) REFERENCES functor_tags (tag) ON DELETE CASCADE -); - -CREATE TABLE related_functors ( - functor_id TEXT NOT NULL, - related_functor_id TEXT NOT NULL, - PRIMARY KEY (functor_id, related_functor_id), - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (related_functor_id) REFERENCES functors (id) ON DELETE CASCADE -); - -CREATE TABLE functor_comments ( - id INTEGER PRIMARY KEY, - functor_id TEXT NOT NULL, - comment TEXT NOT NULL, - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE -); - -CREATE INDEX idx_functor_comments ON functor_comments (functor_id); diff --git a/databases/catdat/schema/010_functor-properties.sql b/databases/catdat/schema/010_functor-properties.sql deleted file mode 100644 index f1dbec5d1..000000000 --- a/databases/catdat/schema/010_functor-properties.sql +++ /dev/null @@ -1,51 +0,0 @@ -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, - required_source TEXT, - required_target TEXT, - FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT, - FOREIGN KEY (dual_property_id) REFERENCES functor_properties (id) ON DELETE SET NULL, - FOREIGN KEY (required_source) REFERENCES categories (id) ON DELETE SET NULL, - FOREIGN KEY (required_target) REFERENCES categories (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX functor_properties_lower_id_unique ON functor_properties (lower(id)); - -CREATE INDEX idx_functor_properties_required_source -ON functor_properties(required_source) -WHERE required_source IS NOT NULL; - -CREATE INDEX idx_functor_properties_required_target -ON functor_properties(required_target) -WHERE required_target IS NOT NULL; - -CREATE TABLE related_functor_properties ( - property_id TEXT NOT NULL, - related_property_id TEXT NOT NULL, - PRIMARY KEY (property_id, related_property_id), - FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE, - FOREIGN KEY (related_property_id) REFERENCES functor_properties (id) ON DELETE CASCADE -); - -CREATE TABLE functor_property_assignments ( - id INTEGER PRIMARY KEY, - functor_id TEXT NOT NULL, - property_id TEXT NOT NULL, - is_satisfied INTEGER - -- we use NULL for undecidable properties - CHECK (is_satisfied in (TRUE, FALSE, NULL)), - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_deduced INTEGER NOT NULL DEFAULT FALSE - CHECK (is_deduced in (TRUE, FALSE)), - check_redundancy INTEGER NOT NULL DEFAULT TRUE - CHECK (check_redundancy in (TRUE, FALSE)), - UNIQUE (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 -); - -CREATE INDEX idx_property_functor ON functor_property_assignments (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/011_functor-implications.sql b/databases/catdat/schema/011_functor-implications.sql deleted file mode 100644 index 9d505cd1f..000000000 --- a/databases/catdat/schema/011_functor-implications.sql +++ /dev/null @@ -1,53 +0,0 @@ -CREATE TABLE functor_implications ( - id TEXT PRIMARY KEY, - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_equivalence INTEGER NOT NULL DEFAULT FALSE, - is_deduced INTEGER NOT NULL DEFAULT FALSE, - dualized_from TEXT, - CHECK (dualized_from IS NULL OR is_deduced = TRUE), - FOREIGN KEY (dualized_from) REFERENCES functor_implications (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX functor_implications_lower_id_unique ON functor_implications (lower(id)); - -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 category_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 category_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/databases/catdat/schema/012_functor-implications-view.sql b/databases/catdat/schema/012_functor-implications-view.sql deleted file mode 100644 index c75256ccd..000000000 --- a/databases/catdat/schema/012_functor-implications-view.sql +++ /dev/null @@ -1,71 +0,0 @@ -CREATE VIEW functor_implications_view AS -SELECT - i.id, - i.is_equivalence, - i.proof, - 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 TRIGGER trg_functor_implications_view_insert -INSTEAD OF INSERT ON functor_implications_view -BEGIN - INSERT INTO functor_implications - (id, is_equivalence, proof, is_deduced, dualized_from) - VALUES ( - NEW.id, - COALESCE(NEW.is_equivalence, FALSE), - NEW.proof, - 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/databases/catdat/schema/013_adjoint-functors.sql b/databases/catdat/schema/013_adjoint-functors.sql deleted file mode 100644 index dfb40a436..000000000 --- a/databases/catdat/schema/013_adjoint-functors.sql +++ /dev/null @@ -1,26 +0,0 @@ -CREATE TABLE adjoint_functors ( - left_adjoint TEXT NOT NULL, - right_adjoint TEXT NOT NULL, - PRIMARY KEY (left_adjoint, right_adjoint), - UNIQUE (left_adjoint), - UNIQUE (right_adjoint), - FOREIGN KEY (left_adjoint) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (right_adjoint) REFERENCES functors (id) ON DELETE CASCADE -); - -CREATE TRIGGER adjoint_functors_source_target_check_insert -BEFORE INSERT ON adjoint_functors -BEGIN - SELECT - CASE - WHEN ( - (SELECT source FROM functors WHERE id = NEW.left_adjoint) != - (SELECT target FROM functors WHERE id = NEW.right_adjoint) - ) - OR ( - (SELECT target FROM functors WHERE id = NEW.left_adjoint) != - (SELECT source FROM functors WHERE id = NEW.right_adjoint) - ) - THEN RAISE(ABORT, 'Adjoint functors must have reversed source/target') - END; -END; \ No newline at end of file diff --git a/databases/catdat/scripts/config.ts b/databases/catdat/scripts/config.ts index 1c592c59a..c887f69ba 100644 --- a/databases/catdat/scripts/config.ts +++ b/databases/catdat/scripts/config.ts @@ -1,8 +1,10 @@ export type StructureType = 'category' | 'functor' -export const STRUCTURES: StructureType[] = ['category', 'functor'] - export const PLURALS = { category: 'categories', functor: 'functors', -} +} as const + +export const STRUCTURES: StructureType[] = ['category', 'functor'] + +export const STRUCTURES_WITH_DUALS: StructureType[] = ['category'] diff --git a/databases/catdat/scripts/deduce-category-implications.ts b/databases/catdat/scripts/deduce-category-implications.ts deleted file mode 100644 index ce54aefee..000000000 --- a/databases/catdat/scripts/deduce-category-implications.ts +++ /dev/null @@ -1,120 +0,0 @@ -import { get_client } from './utils/helpers' -import { clear_deduced_implications, is_dualizable } from './utils/implications' - -const db = get_client() - -/** - * Deduces category implications from given ones. - */ -export function deduce_category_implications() { - console.info('\n--- Deduce category implications ---') - clear_deduced_implications(db, 'category') - create_dualized_category_implications() - create_self_dual_category_implications() -} - -/** - * Dualizes all implications of categories by dualizing the involved properties - * (in case they have a dual). For example, if P ===> Q holds, - * then P^op ===> Q^op holds as well. - */ -function create_dualized_category_implications() { - const implications_query = db.prepare< - never[], - { - id: string - assumptions: string - conclusions: string - dual_assumptions: string - dual_conclusions: string - is_equivalence: 0 | 1 - } - >( - `SELECT - v.id, - v.assumptions, - v.conclusions, - v.is_equivalence, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.assumptions) a - JOIN category_properties p ON p.id = a.value - ) AS dual_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.conclusions) c - JOIN category_properties p ON p.id = c.value - ) AS dual_conclusions - FROM category_implications_view v - WHERE v.is_deduced = FALSE`, - ) - - const implications = implications_query.all() - - const dualizable_implications = implications.filter(is_dualizable) - - const insert_query = db.prepare( - `INSERT INTO category_implications_view ( - id, - assumptions, - conclusions, - is_equivalence, - is_deduced, - dualized_from, - proof - ) VALUES (?, ?, ?, ?, TRUE, ?, ?)`, - ) - - const insert_duals = db.transaction(() => { - for (const impl of dualizable_implications) { - insert_query.run( - `dual_${impl.id}`, - impl.dual_assumptions, - impl.dual_conclusions, - impl.is_equivalence, - impl.id, - 'This follows from the dual implication.', - ) - } - }) - - insert_duals() - - console.info(`Deduced ${dualizable_implications.length} implications by duality`) -} - -/** - * Creates all trivial implications of the form - * self-dual + P ===> P^op - */ -function create_self_dual_category_implications() { - const rows = db - .prepare( - `INSERT INTO category_implications_view ( - id, - assumptions, - conclusions, - is_equivalence, - proof, - is_deduced - ) - SELECT - 'self-dual_' || p.id, - json_array('self-dual', p.id), - json_array(p.dual_property_id), - FALSE, - 'This holds by self-duality.', - TRUE - FROM - category_properties p - WHERE - p.dual_property_id IS NOT NULL - AND p.id != 'self-dual' - AND p.id != p.dual_property_id - AND p.invariant_under_equivalences = TRUE - RETURNING id`, - ) - .all() - - console.info(`Deduced ${rows.length} implications by self-duality`) -} diff --git a/databases/catdat/scripts/deduce-functor-implications.ts b/databases/catdat/scripts/deduce-functor-implications.ts deleted file mode 100644 index 85546642e..000000000 --- a/databases/catdat/scripts/deduce-functor-implications.ts +++ /dev/null @@ -1,100 +0,0 @@ -import { get_client } from './utils/helpers' -import { clear_deduced_implications, is_dualizable } from './utils/implications' - -const db = get_client() - -/** - * Deduces functor implications from given ones. - */ -export function deduce_functor_implications() { - console.info('\n--- Deduce functor implications ---') - clear_deduced_implications(db, 'functor') - create_dualized_functor_implications() -} - -/** - * Dualizes all implications of functors by dualizing the involved properties - * (in case they have a dual). For example, if P ===> Q holds, - * then P^op ===> Q^op holds as well. The assumptions of source and target - * categories (if any) need to be dualized as well. - */ -function create_dualized_functor_implications() { - const implications_query = db.prepare< - never[], - { - id: string - assumptions: string - conclusions: string - dual_assumptions: string - dual_source_assumptions: string - dual_target_assumptions: string - dual_conclusions: string - is_equivalence: 0 | 1 - } - >( - `SELECT - v.id, - v.assumptions, - v.conclusions, - v.is_equivalence, - ( - 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 category_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 category_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 = implications_query.all() - - const dualizable_implications = implications.filter(is_dualizable) - - const insert_query = db.prepare( - `INSERT INTO functor_implications_view ( - id, - assumptions, - source_assumptions, - target_assumptions, - conclusions, - is_equivalence, - is_deduced, - dualized_from, - proof - ) VALUES (?, ?, ?, ?, ?, ?, TRUE, ?, ?)`, - ) - - const insert_duals = db.transaction(() => { - for (const impl of dualizable_implications) { - insert_query.run( - `dual_${impl.id}`, - impl.dual_assumptions, - impl.dual_source_assumptions, - impl.dual_target_assumptions, - impl.dual_conclusions, - impl.is_equivalence, - impl.id, - 'This follows from the dual implication.', - ) - } - }) - - insert_duals() - - console.info(`Deduced ${dualizable_implications.length} implications by duality`) -} diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts new file mode 100644 index 000000000..c8f8e06de --- /dev/null +++ b/databases/catdat/scripts/deduce-implications.ts @@ -0,0 +1,204 @@ +import { STRUCTURES_WITH_DUALS, type StructureType } from './config' +import { are_equal_sets, parse_nested_json_set, parse_json_set } from './utils/helpers' +import { get_client } from './utils/db' + +const db = get_client() + +/** + * Clears all deduced implications. This is done before the deduction starts. + */ +export function clear_deduced_implications(type: StructureType) { + console.info(`\n--- Deduce ${type} implications ---`) + db.prepare(`DELETE FROM implications WHERE is_deduced = TRUE AND type = ?`).run(type) +} + +/** + * Dualizes all implications by dualizing the involved properties + * (in case they have a dual). For example, if P ===> Q holds, + * then P^op ===> Q^op holds as well. + */ +export function create_dualized_implications(type: StructureType) { + const structure_maps = db + .prepare<[StructureType], { map: string; mapped_type: StructureType }>( + `SELECT map, mapped_type + FROM structure_maps WHERE type = ?`, + ) + .all(type) + + const implications_query = db.prepare< + [StructureType], + { + id: string + is_equivalence: 0 | 1 + assumptions: string + conclusions: string + dual_assumptions: string + dual_conclusions: string + dual_mapped_assumptions: string + } + >( + `SELECT + i.id, + i.is_equivalence, + i.assumptions, + i.conclusions, + ( + SELECT json_group_array(p.dual_property_id) + FROM assumptions a + LEFT JOIN properties p ON p.id = a.property_id + WHERE a.implication_id = i.id + ) AS dual_assumptions, + ( + SELECT json_group_array(p.dual_property_id) + FROM conclusions a + LEFT JOIN properties p ON p.id = a.property_id + WHERE a.implication_id = i.id + ) AS dual_conclusions, + ( + SELECT json_group_object(map, properties) + FROM ( + SELECT + a.map, + json_group_array(p.dual_property_id) AS properties + FROM mapped_assumptions a + INNER JOIN properties p ON p.id = a.property_id + WHERE a.implication_id = i.id + GROUP BY a.map + ) + ) AS dual_mapped_assumptions + FROM implications_view i + WHERE i.type = ? AND i.is_deduced = FALSE`, + ) + + const implications = implications_query.all(type) + + const implication_insert = db.prepare(` + INSERT INTO implications + (id, type, is_equivalence, proof, is_deduced, dualized_from) + VALUES (?, ?, ?, ?, TRUE, ?) + `) + + const assumption_insert = db.prepare(` + INSERT INTO assumptions (implication_id, property_id, type) + VALUES (?, ?, ?) + `) + + const conclusion_insert = db.prepare(` + INSERT INTO conclusions (implication_id, property_id, type) + VALUES (?, ?, ?) + `) + + const mapped_assumption_insert = db.prepare(` + INSERT INTO mapped_assumptions + (implication_id, map, property_id, type, property_type) + VALUES (?, ?, ?, ?, ?) + `) + + const insert_duals = db.transaction(() => { + let count = 0 + + for (const impl of implications) { + const dual_id = `dual_${impl.id}` + + const assumptions = parse_json_set(impl.assumptions) + const dual_assumptions = parse_json_set(impl.dual_assumptions) + const conclusions = parse_json_set(impl.conclusions) + const dual_conclusions = parse_json_set(impl.dual_conclusions) + const dual_mapped_assumptions = parse_nested_json_set( + impl.dual_mapped_assumptions, + ) + + if (dual_assumptions.has(null)) continue + if (dual_conclusions.has(null)) continue + + if (Object.values(dual_mapped_assumptions).some((set) => set?.has(null))) { + continue + } + + if ( + are_equal_sets(assumptions, dual_assumptions) && + are_equal_sets(conclusions, dual_conclusions) + ) { + continue + } + + count++ + + implication_insert.run( + dual_id, + type, + impl.is_equivalence, + 'This follows from the dual implication.', + impl.id, + ) + + for (const a of dual_assumptions) { + assumption_insert.run(dual_id, a, type) + } + + for (const c of dual_conclusions) { + conclusion_insert.run(dual_id, c, type) + } + + for (const { map, mapped_type } of structure_maps) { + const duals = dual_mapped_assumptions[map] + for (const d of duals ?? []) { + mapped_assumption_insert.run(dual_id, map, d, type, mapped_type) + } + } + } + + console.info(`Deduced ${count} ${type} implications by duality`) + }) + + insert_duals() +} + +/** + * Creates all trivial implications of the form "self-dual + P ===> P^op". + */ +export function create_self_dual_implications(type: StructureType) { + if (!STRUCTURES_WITH_DUALS.includes(type)) return + + const relevant_props = db + .prepare<[StructureType], { id: string; dual: string }>( + `SELECT + id, + dual_property_id AS dual + FROM properties + WHERE + type = ? + AND dual_property_id IS NOT NULL + AND id != dual_property_id + AND invariant_under_equivalences = TRUE`, + ) + .all(type) + + const implication_insert = db.prepare(` + INSERT INTO implications + (id, type, proof, is_deduced) + VALUES (?, ?, 'This holds by self-duality.', TRUE) + `) + + const assumption_insert = db.prepare(` + INSERT INTO assumptions + (implication_id, property_id, type) + VALUES (?, ?, ?) + `) + + const conclusion_insert = db.prepare(` + INSERT INTO conclusions + (implication_id, property_id, type) + VALUES (?, ?, ?) + `) + + for (const p of relevant_props) { + const implication_id = `self-dual_${p.id}` + implication_insert.run(implication_id, type) + assumption_insert.run(implication_id, p.id, type) + assumption_insert.run(implication_id, 'self-dual', type) + conclusion_insert.run(implication_id, p.dual, type) + } + + console.info(`Deduced ${relevant_props.length} ${type} implications by self-duality`) +} diff --git a/databases/catdat/scripts/deduce-special-morphisms.ts b/databases/catdat/scripts/deduce-special-morphisms.ts index 8e09db96e..957f0cc16 100644 --- a/databases/catdat/scripts/deduce-special-morphisms.ts +++ b/databases/catdat/scripts/deduce-special-morphisms.ts @@ -1,4 +1,4 @@ -import { get_client } from './utils/helpers' +import { get_client } from './utils/db' const db = get_client() @@ -18,19 +18,18 @@ export function deduce_special_morphisms() { function deduce_special_morphisms_of_dual_categories() { const res = db .prepare( - ` - INSERT INTO special_morphisms (category_id, type, description, proof) - SELECT - c.dual_category_id, - t.dual, - m.description, - 'This is deduced from its dual category.' - FROM categories c - INNER JOIN special_morphisms m ON m.category_id = c.id - INNER JOIN special_morphism_types t ON t.type = m.type - WHERE c.dual_category_id IS NOT NULL - ON CONFLICT DO NOTHING - `, + `INSERT INTO special_morphisms + (category_id, type, description, proof) + SELECT + c.dual_structure_id, + t.dual, + m.description, + 'This is deduced from its dual category.' + FROM structures c + INNER JOIN special_morphisms m ON m.category_id = c.id + INNER JOIN special_morphism_types t ON t.type = m.type + WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL + ON CONFLICT DO NOTHING`, ) .run() diff --git a/databases/catdat/scripts/deduce-special-objects.ts b/databases/catdat/scripts/deduce-special-objects.ts index 966f582a4..5904215cb 100644 --- a/databases/catdat/scripts/deduce-special-objects.ts +++ b/databases/catdat/scripts/deduce-special-objects.ts @@ -1,4 +1,4 @@ -import { get_client } from './utils/helpers' +import { get_client } from './utils/db' const db = get_client() @@ -16,13 +16,13 @@ async function deduce_special_objects_of_dual_categories() { .prepare( `INSERT INTO special_objects (category_id, type, description) SELECT - c.dual_category_id, + c.dual_structure_id, t.dual, o.description - FROM categories c + FROM structures c INNER JOIN special_objects o ON o.category_id = c.id INNER JOIN special_object_types t ON t.type = o.type - WHERE c.dual_category_id IS NOT NULL + WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL ON CONFLICT DO NOTHING`, ) .run() diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 014a27c7b..12fcc03f2 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -4,19 +4,21 @@ */ import { type Database, SqliteError } from 'better-sqlite3' -import { get_client, is_subset } from './utils/helpers' +import { is_subset } from './utils/helpers' +import { get_client } from './utils/db' import { - get_structures, - get_normalized_implications, get_properties_dict, get_property_assignments, - is_dual_structure, - type StructureMeta, - type NormalizedImplication, type PropertyMeta, -} from './utils/deduction' -import { get_contradiction_string, get_proof_string } from './utils/implications' -import type { StructureType } from './config' +} from './utils/properties' +import { + get_contradiction_string, + get_normalized_implications, + get_proof_string, + NormalizedImplication, +} from './utils/implications' +import { STRUCTURES_WITH_DUALS, type StructureType } from './config' +import { get_structures, is_dual_structure, type StructureMeta } from './utils/structures' /** * Returns the set of satisfied properties that can be deduced from a set @@ -31,7 +33,6 @@ export function get_deduced_satisfied_properties( stop_when_found?: string }, type: StructureType, - // used for source and target properties of a functor associated_satisfied_properties?: Record>, ) { const found = new Set() @@ -49,15 +50,15 @@ export function get_deduced_satisfied_properties( if (!is_valid) continue - if (implication.associated_assumptions) { - const is_applicable = Object.keys( - implication.associated_assumptions, - ).every((key) => { - return is_subset( - implication.associated_assumptions?.[key] ?? new Set(), - associated_satisfied_properties?.[key] ?? new Set(), - ) - }) + if (implication.mapped_assumptions) { + const is_applicable = Object.keys(implication.mapped_assumptions).every( + (key) => { + return is_subset( + implication.mapped_assumptions?.[key] ?? new Set(), + associated_satisfied_properties?.[key] ?? new Set(), + ) + }, + ) if (!is_applicable) continue } @@ -101,7 +102,6 @@ export function get_deduced_unsatisfied_properties( stop_when_found?: string }, type: StructureType, - // used for source and target properties of a functor associated_satisfied_properties?: Record>, ) { const found = new Set() @@ -122,12 +122,12 @@ export function get_deduced_unsatisfied_properties( }) if (!is_valid) continue - if (implication.associated_assumptions) { + if (implication.mapped_assumptions) { const is_applicable = Object.keys( - implication.associated_assumptions, + implication.mapped_assumptions, ).every((key) => { return is_subset( - implication.associated_assumptions?.[key] ?? new Set(), + implication.mapped_assumptions?.[key] ?? new Set(), associated_satisfied_properties?.[key] ?? new Set(), ) }) @@ -180,14 +180,14 @@ function save_satisfied_properties( const err_msg = `❌ Failed to complete deduction of satisfied properties for ${structure_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` const property_insert = db.prepare(` - INSERT INTO ${type}_property_assignments - (${type}_id, property_id, is_satisfied, proof, is_deduced) - VALUES (?, ?, TRUE, ?, TRUE) + INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, proof, is_deduced) + VALUES (?, ?, ?, TRUE, ?, TRUE) `) try { for (const p of found) { - property_insert.run(structure_id, p, proofs[p]) + property_insert.run(structure_id, p, type, proofs[p]) } } catch (err) { if (err instanceof SqliteError) { @@ -217,14 +217,14 @@ function save_unsatisfied_properties( const err_msg = `❌ Failed to complete deduction of unsatisfied properties for ${structure_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` const property_insert = db.prepare(` - INSERT INTO ${type}_property_assignments - (${type}_id, property_id, is_satisfied, proof, is_deduced) - VALUES (?, ?, FALSE, ?, TRUE) + INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, proof, is_deduced) + VALUES (?, ?, ?, FALSE, ?, TRUE) `) try { for (const p of found) { - property_insert.run(structure_id, p, proofs[p]) + property_insert.run(structure_id, p, type, proofs[p]) } } catch (err) { if (err instanceof SqliteError) { @@ -312,7 +312,7 @@ function deduce_dual_properties( dual_unsatisfied: Set, dual_undecidable: Set, properties_dict: Record, - type: 'category', + type: StructureType, ) { const new_satisfied = new Set() @@ -342,9 +342,9 @@ function deduce_dual_properties( } const property_insert = db.prepare(` - INSERT INTO ${type}_property_assignments - (${type}_id, property_id, is_satisfied, proof, is_deduced) - VALUES (?, ?, ?, ?, TRUE) + INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, proof, is_deduced) + VALUES (?, ?, ?, ?, ?, TRUE) `) const proof_satisfied = `Its dual ${type} satisfies the dual property.` @@ -352,7 +352,7 @@ function deduce_dual_properties( const proof_undecidable = `The dual property is undecidable for its dual ${type}.` for (const p of new_satisfied) { - property_insert.run(structure.id, p, 1, proof_satisfied) + property_insert.run(structure.id, p, type, 1, proof_satisfied) } console.info( @@ -360,7 +360,7 @@ function deduce_dual_properties( ) for (const q of new_unsatisfied) { - property_insert.run(structure.id, q, 0, proof_unsatisfied) + property_insert.run(structure.id, q, type, 0, proof_unsatisfied) } console.info( @@ -368,7 +368,7 @@ function deduce_dual_properties( ) for (const q of new_undecidable) { - property_insert.run(structure.id, q, null, proof_undecidable) + property_insert.run(structure.id, q, type, null, proof_undecidable) } console.info( @@ -380,13 +380,14 @@ function deduce_dual_properties( * Clears all the deduced properties. This runs before the deduction starts. */ function delete_deduced_properties(db: Database, type: StructureType) { - db.prepare(`DELETE FROM ${type}_property_assignments WHERE is_deduced = TRUE`).run() + db.prepare( + `DELETE FROM property_assignments WHERE is_deduced = TRUE AND type = ?`, + ).run(type) } /** - * --- MAIN FUNCTION --- - * Deduce properties of structures from given ones - * by using the list of implications. + * Main function: Deduce properties of structures from given ones + * by using the stored implications. */ export function deduce_properties_for_structures(type: StructureType) { console.info(`\n--- Deduce ${type} properties ---`) @@ -427,8 +428,7 @@ export function deduce_properties_for_structures(type: StructureType) { deduction() - // currently, only categories have duals - if (type !== 'category') return + if (!STRUCTURES_WITH_DUALS.includes(type)) return const dual_deduction = db.transaction(() => { for (const structure of structures) { diff --git a/databases/catdat/scripts/deduce.ts b/databases/catdat/scripts/deduce.ts index f0c726144..b68f7ea04 100644 --- a/databases/catdat/scripts/deduce.ts +++ b/databases/catdat/scripts/deduce.ts @@ -1,9 +1,12 @@ -import { deduce_category_implications } from './deduce-category-implications' -import { deduce_functor_implications } from './deduce-functor-implications' import { deduce_special_objects } from './deduce-special-objects' import { deduce_special_morphisms } from './deduce-special-morphisms' import { deduce_properties_for_structures } from './deduce-structure-properties' -import { restrict_functor_properties } from './restrict-functor-properties' +import { restrict_representable_functors } from './restrict-functor-properties' +import { + clear_deduced_implications, + create_dualized_implications, + create_self_dual_implications, +} from './deduce-implications' deduce() @@ -11,13 +14,17 @@ deduce() * Makes deductions for categories and functors. */ function deduce() { - deduce_category_implications() + // --- categories --- + clear_deduced_implications('category') + create_dualized_implications('category') + create_self_dual_implications('category') deduce_properties_for_structures('category') - deduce_special_objects() deduce_special_morphisms() - restrict_functor_properties() - deduce_functor_implications() + // --- functors --- + restrict_representable_functors() + clear_deduced_implications('functor') + create_dualized_implications('functor') deduce_properties_for_structures('functor') } diff --git a/databases/catdat/scripts/expected-data/decided-categories.json b/databases/catdat/scripts/expected-data/decided-categories.json index 6764d2e0a..4a982575a 100644 --- a/databases/catdat/scripts/expected-data/decided-categories.json +++ b/databases/catdat/scripts/expected-data/decided-categories.json @@ -13,6 +13,7 @@ "Set_op", "Set*", "Top", + "Top_op", "Top*", "Vect", "FinVect_f", diff --git a/databases/catdat/scripts/proof-length.ts b/databases/catdat/scripts/proof-length.ts index 3af494b01..3cac952e4 100644 --- a/databases/catdat/scripts/proof-length.ts +++ b/databases/catdat/scripts/proof-length.ts @@ -1,5 +1,5 @@ -import { PLURALS, type StructureType } from './config' -import { get_client } from './utils/helpers' +import { type StructureType } from './config' +import { get_client } from './utils/db' const db = get_client() @@ -20,20 +20,23 @@ function report_long_proofs() { function report_long_property_proofs(type: StructureType) { const long_proofs = db - .prepare<[number], { id: string; property: string; length: number }>( + .prepare< + [StructureType, number], + { id: string; property: string; length: number } + >( `SELECT - ${type}_id AS id, + structure_id AS id, property_id AS property, length(proof) AS length - FROM ${type}_property_assignments - WHERE is_deduced = FALSE AND length(proof) >= ? + FROM property_assignments + WHERE type = ? AND is_deduced = FALSE AND length(proof) >= ? ORDER BY length(proof) DESC`, ) - .all(PROOF_LENGTH_THRESHOLD) + .all(type, PROOF_LENGTH_THRESHOLD) if (!long_proofs.length) return - console.info(`\n--- Long property proofs for ${PLURALS[type]} ---`) + console.info(`\n--- Long property proofs (type: ${type}) ---`) for (const { id, property, length } of long_proofs) { console.warn( @@ -44,19 +47,22 @@ function report_long_property_proofs(type: StructureType) { function report_long_implication_proofs(type: StructureType) { const long_proofs = db - .prepare<[number], { id: string; length: number }>( + .prepare<[StructureType, number], { id: string; length: number }>( `SELECT id, length(proof) AS length - FROM ${type}_implications - WHERE is_deduced = FALSE AND length(proof) >= ? + FROM implications + WHERE + type = ? + AND is_deduced = FALSE + AND length(proof) >= ? ORDER BY length(proof) DESC`, ) - .all(PROOF_LENGTH_THRESHOLD) + .all(type, PROOF_LENGTH_THRESHOLD) if (!long_proofs.length) return - console.info(`\n--- Long implication proofs for ${PLURALS[type]} ---`) + console.info(`\n--- Long implication proofs (type: ${type}) ---`) for (const { id, length } of long_proofs) { console.warn( diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index f7f4e6408..d0f6d6be0 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -1,16 +1,15 @@ -import { get_client } from './utils/helpers' -import { - get_categories, - get_normalized_category_implications, - type NormalizedCategoryImplication, -} from './utils/categories' +import { get_client } from './utils/db' import { get_deduced_satisfied_properties, get_deduced_unsatisfied_properties, } from './deduce-structure-properties' -import { get_property_assignments_by_deduction, StructureMeta } from './utils/deduction' -import { get_functors, get_normalized_functor_implications } from './utils/functors' -import { StructureType } from './config' +import { get_property_assignments_by_deduction } from './utils/properties' +import type { StructureType } from './config' +import { + get_normalized_implications, + type NormalizedImplication, +} from './utils/implications' +import { get_structures } from './utils/structures' const db = get_client() @@ -33,14 +32,9 @@ function check_redundancies() { function check_redundant_property_assignments(type: StructureType) { console.info(`\n--- Check redundant ${type} property assignments ---`) - // TODO: refactor this when > 2 types of structures are available - const implications = - type === 'category' - ? get_normalized_category_implications(db) - : get_normalized_functor_implications(db) + const implications = get_normalized_implications(db, type) - const structures: StructureMeta[] = - type === 'category' ? get_categories(db) : get_functors(db) + const structures = get_structures(db, type) const assignments = get_property_assignments_by_deduction(db, structures, type) const ignore_dict = get_ignored_redundant_assignments(type) @@ -112,7 +106,7 @@ function check_redundant_property_assignments(type: StructureType) { function get_redundant_satisfied_property( type: StructureType, satisfied_properties: Set, - implications: NormalizedCategoryImplication[], + implications: NormalizedImplication[], ignored: Set = new Set(), associated_satisfied_properties?: Record>, ) { @@ -142,7 +136,7 @@ function get_redundant_unsatisfied_property( type: StructureType, satisfied_properties: Set, unsatisfied_properties: Set, - implications: NormalizedCategoryImplication[], + implications: NormalizedImplication[], ignored: Set = new Set(), associated_satisfied_properties?: Record>, ) { @@ -170,12 +164,12 @@ function get_redundant_unsatisfied_property( */ function get_ignored_redundant_assignments(type: StructureType) { const rows = db - .prepare( - `SELECT ${type}_id AS structure_id, property_id - FROM ${type}_property_assignments - WHERE check_redundancy = FALSE`, + .prepare<[StructureType], { structure_id: string; property_id: string }>( + `SELECT structure_id, property_id + FROM property_assignments + WHERE check_redundancy = FALSE AND type = ?`, ) - .all() + .all(type) const grouped: Record> = {} diff --git a/databases/catdat/scripts/restrict-functor-properties.ts b/databases/catdat/scripts/restrict-functor-properties.ts index c3c067328..e755fa45c 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -1,41 +1,38 @@ -import { get_client } from './utils/helpers' +import { get_client } from './utils/db' const db = get_client() /** - * Ensures that selected properties of functors are restricted - * to specified source and target categories. + * Ensures that only functors with target Set are representable. + * When necessary, this can be extended to other properties in the future. */ -export function restrict_functor_properties() { - console.info('\n--- Restrict functor properties ---') +export function restrict_representable_functors() { + console.info('\n--- Restrict representable functors ---') - for (const domain of ['source', 'target']) { - const res = db - .prepare( - `INSERT INTO functor_property_assignments ( - functor_id, - property_id, - is_satisfied, - proof, - is_deduced, - check_redundancy - ) - SELECT - f.id, - p.id, - FALSE, - 'The ${domain} category is not ' || c.notation || '.', - FALSE, - FALSE - FROM functor_properties p - INNER JOIN categories c ON c.id = p.required_${domain} - JOIN functors f - WHERE f.${domain} <> p.required_${domain}`, - ) - .run() - - console.info( - `Restricted ${res.changes} functor properties based on their required ${domain}`, + const res = db + .prepare( + `INSERT INTO property_assignments ( + structure_id, + property_id, + type, + is_satisfied, + proof, + is_deduced, + check_redundancy + ) + SELECT + f.id, + 'representable', + 'functor', + FALSE, + 'The target category is not $\\Set$.', + FALSE, + FALSE + FROM functors f + WHERE f.target <> 'Set' + ON CONFLICT (structure_id, property_id) DO NOTHING`, ) - } + .run() + + console.info(`Deduced that ${res.changes} functors cannot be representable`) } diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index cda73c402..20aa3f024 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -1,17 +1,17 @@ import path from 'node:path' -import { get_client, seed_file, seed_files } from './utils/helpers' +import { seed_file, seed_files } from './utils/seed.helpers' +import { get_client } from './utils/db' import type { CategoryYaml, ConfigYaml, - CategoryPropertyYaml, - CategoryImplicationYaml, - FunctorImplicationYaml, - FunctorPropertyYaml, + ImplicationYaml, FunctorYaml, PropertyEntry, -} from './seed.types' + StructureYaml, + PropertyYaml, +} from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' -import { PLURALS, STRUCTURES } from './config' +import { PLURALS, STRUCTURES, type StructureType } from './config' const db = get_client() @@ -25,6 +25,25 @@ seed() function seed() { console.info('\n--- Seed CatDat database ---') + check_schema() + clear_all_tables() + seed_config() + + seed_properties({ type: 'category', folder: 'category-properties' }) + seed_implications({ type: 'category', folder: 'category-implications' }) + seed_structures({ type: 'category', folder: 'categories', extra: insert_category }) + + seed_properties({ type: 'functor', folder: 'functor-properties' }) + seed_implications({ type: 'functor', folder: 'functor-implications' }) + seed_structures({ type: 'functor', folder: 'functors', extra: insert_functor }) +} + +/** + * Checks if the schema is up-to-date, and throws an error otherwise. + */ +function check_schema() { + console.info(`\nCheck schema ...`) + const schema_hash = get_saved_schema_hash() const actual_hash = create_schema_hash() @@ -32,18 +51,6 @@ function seed() { console.error(`❌ Your schema appears to be outdated. Run first pnpm db:setup.`) process.exit(1) } - - clear_all_tables() - - seed_config() - - seed_category_properties() - seed_category_implications() - seed_categories() - - seed_functor_properties() - seed_functor_implications() - seed_functors() } /** @@ -53,34 +60,30 @@ function clear_all_tables() { console.info(`\nClear all tables ...`) const tx = db.transaction(() => { - db.pragma('foreign_keys = OFF') + db.pragma('defer_foreign_keys = ON') db.prepare(`DELETE FROM special_morphisms`).run() db.prepare(`DELETE FROM special_morphism_types`).run() db.prepare(`DELETE FROM special_objects`).run() db.prepare(`DELETE FROM special_object_types`).run() - db.prepare(`DELETE FROM functor_implication_source_assumptions`).run() - db.prepare(`DELETE FROM functor_implication_target_assumptions`).run() - db.prepare(`DELETE FROM adjoint_functors`).run() + db.prepare(`DELETE FROM mapped_assumptions`).run() + db.prepare(`DELETE FROM assumptions`).run() + db.prepare(`DELETE FROM conclusions`).run() + db.prepare(`DELETE FROM implications`).run() - for (const type of STRUCTURES) { - const plural = PLURALS[type] - - db.prepare(`DELETE FROM ${type}_implication_assumptions`).run() - db.prepare(`DELETE FROM ${type}_implication_conclusions`).run() - db.prepare(`DELETE FROM ${type}_implications`).run() - db.prepare(`DELETE FROM ${type}_property_assignments`).run() - db.prepare(`DELETE FROM ${type}_comments`).run() - db.prepare(`DELETE FROM related_${plural}`).run() - db.prepare(`DELETE FROM ${type}_tag_assignments`).run() - db.prepare(`DELETE FROM related_${type}_properties`).run() - db.prepare(`DELETE FROM ${type}_properties`).run() - db.prepare(`DELETE FROM ${plural}`).run() - db.prepare(`DELETE FROM ${type}_tags`).run() - } + db.prepare(`DELETE FROM property_assignments`).run() + db.prepare(`DELETE FROM related_properties`).run() + db.prepare(`DELETE FROM properties`).run() + db.prepare(`DELETE FROM related_structures`).run() + db.prepare(`DELETE FROM structure_comments`).run() + db.prepare(`DELETE FROM structure_tag_assignments`).run() + db.prepare(`DELETE FROM tags`).run() db.prepare(`DELETE FROM relations`).run() + + // this deletes categories and functors automatically + db.prepare(`DELETE FROM structures`).run() }) try { @@ -95,8 +98,9 @@ function clear_all_tables() { * Seeds the data from the global config file `config.yaml`. */ function seed_config() { - const category_tag_insert = db.prepare(`INSERT INTO category_tags (tag) VALUES (?)`) - const functor_tag_insert = db.prepare(`INSERT INTO functor_tags (tag) VALUES (?)`) + const tag_insert = db.prepare<[string, StructureType]>( + `INSERT INTO tags (tag, type) VALUES (?, ?)`, + ) const relation_insert = db.prepare( `INSERT INTO relations (relation, conditional) VALUES (?, ?)`, @@ -111,17 +115,14 @@ function seed_config() { ) function insert_config(config: ConfigYaml) { - for (const tag of config.shared_tags) { - category_tag_insert.run(tag) - functor_tag_insert.run(tag) - } - - for (const tag of config.category_tags) { - category_tag_insert.run(tag) - } + for (const type of STRUCTURES) { + for (const tag of config.shared_tags) { + tag_insert.run(tag, type) + } - for (const tag of config.functor_tags) { - functor_tag_insert.run(tag) + for (const tag of config[`${type}_tags`]) { + tag_insert.run(tag, type) + } } for (const { relation, conditional } of config.relations) { @@ -141,136 +142,57 @@ function seed_config() { } /** - * Seeds all properties of categories from YAML files. + * Seeds all structures from YAML files of a given type, + * including their property assignments. */ -function seed_category_properties() { - const property_insert = db.prepare( - `INSERT INTO category_properties ( - id, relation, description, nlab_link, - dual_property_id, invariant_under_equivalences - ) VALUES (?, ?, ?, ?, ?, ?)`, - ) - - const related_insert = db.prepare( - `INSERT INTO related_category_properties - (property_id, related_property_id) - VALUES (?, ?)`, - ) - - function insert_property(property: CategoryPropertyYaml) { - property_insert.run( - property.id, - property.relation, - property.description, - property.nlab_link || null, - property.dual_property || null, - Number(property.invariant_under_equivalences), +function seed_structures({ + type, + folder, + extra, +}: { + type: StructureType + folder: string + extra?: (structure: T) => void +}) { + const structure_insert = db.prepare( + `INSERT INTO structures ( + id, type, name, notation, description, nlab_link, + dual_structure_id ) - - for (const related of property.related_properties) { - related_insert.run(property.id, related) - } - } - - seed_files( - db, - 'category properties', - path.join(data_folder, 'category-properties'), - insert_property, - ) -} - -/** - * Seeds all implications between category properties from YAML files. - */ -function seed_category_implications() { - const implication_insert = db.prepare( - `INSERT INTO category_implications ( - id, proof, is_equivalence - ) VALUES (?, ?, ?)`, - ) - - const assumption_insert = db.prepare( - `INSERT INTO category_implication_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) - - const conclusion_insert = db.prepare( - `INSERT INTO category_implication_conclusions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) - - function insert_implications(implications: CategoryImplicationYaml[]) { - for (const impl of implications) { - implication_insert.run(impl.id, impl.proof, Number(impl.is_equivalence)) - - for (const assumption of impl.assumptions) { - assumption_insert.run(impl.id, assumption) - } - - for (const conclusion of impl.conclusions) { - conclusion_insert.run(impl.id, conclusion) - } - } - } - - seed_files( - db, - 'category implications', - path.join(data_folder, 'category-implications'), - insert_implications, - ) -} - -/** - * Seeds all categories from YAML files, including their property assignments. - */ -function seed_categories() { - const category_insert = db.prepare( - `INSERT INTO categories ( - id, name, notation, objects, morphisms, - description, nlab_link, dual_category_id - ) VALUES (?, ?, ?, ?, ?, ?, ?, ?)`, + VALUES (?, ?, ?, ?, ?, ?, ?)`, ) const tag_insert = db.prepare( - `INSERT INTO category_tag_assignments (category_id, tag) VALUES (?, ?)`, + `INSERT INTO structure_tag_assignments (structure_id, tag, type) + VALUES (?, ?, ?)`, ) const comment_insert = db.prepare( - `INSERT INTO category_comments (category_id, comment) VALUES (?, ?)`, + `INSERT INTO structure_comments (structure_id, comment) + VALUES (?, ?)`, ) const related_insert = db.prepare( - `INSERT INTO related_categories (category_id, related_category_id) VALUES (?, ?)`, - ) - - const special_object_insert = db.prepare( - `INSERT INTO special_objects (category_id, type, description) VALUES (?, ?, ?)`, - ) - - const special_morphism_insert = db.prepare( - `INSERT INTO special_morphisms (category_id, type, description, proof) - VALUES (?, ?, ?, ?)`, + `INSERT INTO related_structures (structure_id, related_structure_id, type) + VALUES (?, ?, ?)`, ) const property_assignment_insert = db.prepare( - `INSERT INTO category_property_assignments ( - category_id, property_id, is_satisfied, proof, check_redundancy - ) VALUES (?, ?, ?, ?, ?)`, + `INSERT INTO property_assignments ( + structure_id, property_id, type, is_satisfied, proof, check_redundancy + ) VALUES (?, ?, ?, ?, ?, ?)`, ) function insert_property_assignments( - category_id: string, + structure_id: string, entries: PropertyEntry[], is_satisfied: 0 | 1 | null, ) { for (const entry of entries) { property_assignment_insert.run( - category_id, + structure_id, entry.property, + type, is_satisfied, entry.proof, entry.check_redundancy === false ? 0 : 1, @@ -278,244 +200,195 @@ function seed_categories() { } } - function insert_category(category: CategoryYaml) { - category_insert.run( - category.id, - category.name, - category.notation, - category.objects, - category.morphisms, - category.description, - category.nlab_link, - category.dual_category || null, + function insert_structure(structure: T) { + structure_insert.run( + structure.id, + type, + structure.name, + structure.notation, + structure.description, + structure.nlab_link, + structure[`dual_${type}`] || null, ) - for (const tag of category.tags) { - tag_insert.run(category.id, tag) - } - - for (const comment of category.comments ?? []) { - comment_insert.run(category.id, comment) - } - - for (const related of category.related_categories) { - related_insert.run(category.id, related) + for (const tag of structure.tags) { + tag_insert.run(structure.id, tag, type) } - for (const [type, entry] of Object.entries(category.special_objects)) { - if (!entry) continue - special_object_insert.run(category.id, type, entry.description) + for (const comment of structure.comments ?? []) { + comment_insert.run(structure.id, comment) } - for (const [type, entry] of Object.entries(category.special_morphisms)) { - if (!entry) continue - special_morphism_insert.run(category.id, type, entry.description, entry.proof) + for (const related of structure[`related_${PLURALS[type]}`] ?? []) { + related_insert.run(structure.id, related, type) } - insert_property_assignments(category.id, category.satisfied_properties, 1) - insert_property_assignments(category.id, category.unsatisfied_properties, 0) + insert_property_assignments(structure.id, structure.satisfied_properties, 1) + insert_property_assignments(structure.id, structure.unsatisfied_properties, 0) insert_property_assignments( - category.id, - category.undecidable_properties ?? [], + structure.id, + structure.undecidable_properties ?? [], null, ) + + if (extra) extra(structure) } - seed_files(db, 'categories', path.join(data_folder, 'categories'), insert_category) + seed_files(db, PLURALS[type], path.join(data_folder, folder), insert_structure) } /** - * Seeds all properties of functors from YAML files. + * Inserts the data of a category that is specific to categories. */ -function seed_functor_properties() { +function insert_category(category: CategoryYaml) { + const category_insert = db.prepare( + `INSERT INTO categories ( + id, objects, morphisms + ) VALUES (?, ?, ?)`, + ) + + const special_object_insert = db.prepare( + `INSERT INTO special_objects (category_id, type, description) VALUES (?, ?, ?)`, + ) + + const special_morphism_insert = db.prepare( + `INSERT INTO special_morphisms (category_id, type, description, proof) + VALUES (?, ?, ?, ?)`, + ) + + category_insert.run(category.id, category.objects, category.morphisms) + + for (const [type, entry] of Object.entries(category.special_objects)) { + if (!entry) continue + special_object_insert.run(category.id, type, entry.description) + } + + for (const [type, entry] of Object.entries(category.special_morphisms)) { + if (!entry) continue + special_morphism_insert.run(category.id, type, entry.description, entry.proof) + } +} + +/** + * Inserts the data of a functor that is specific to functors. + */ +function insert_functor(functor: FunctorYaml) { + const functor_insert = db.prepare( + `INSERT INTO functors (id, source, target, left_adjoint) + VALUES (?, ?, ?, ?)`, + ) + + functor_insert.run( + functor.id, + functor.source, + functor.target, + functor.left_adjoint || null, + ) +} + +/** + * Seeds all properties of a given type from YAML files. + */ +function seed_properties({ type, folder }: { type: StructureType; folder: string }) { const property_insert = db.prepare(` - INSERT INTO functor_properties ( - id, relation, description, - required_source, required_target, + INSERT INTO properties ( + id, type, relation, description, nlab_link, dual_property_id, invariant_under_equivalences - ) VALUES (?, ?, ?, ?, ?, ?, ?, ?)`) + ) VALUES (?, ?, ?, ?, ?, ?, ?)`) const related_insert = db.prepare( - `INSERT INTO related_functor_properties - (property_id, related_property_id) - VALUES (?, ?)`, + `INSERT INTO related_properties + (property_id, related_property_id, type) + VALUES (?, ?, ?)`, ) - function insert_property(property: FunctorPropertyYaml) { + function insert_property(property: PropertyYaml) { property_insert.run( property.id, + type, property.relation, property.description, - property.required_source || null, - property.required_target || null, property.nlab_link || null, property.dual_property || null, Number(property.invariant_under_equivalences), ) for (const related of property.related_properties) { - related_insert.run(property.id, related) + related_insert.run(property.id, related, type) } } seed_files( db, - 'functor properties', - path.join(data_folder, 'functor-properties'), + `properties of ${PLURALS[type]}`, + path.join(data_folder, folder), insert_property, ) } /** - * Seeds all implications between functor properties from YAML files. + * Seeds all implications of a given type from YAML files. */ -function seed_functor_implications() { +function seed_implications({ type, folder }: { type: StructureType; folder: string }) { + const structure_maps = db + .prepare<[StructureType], { map: string; mapped_type: StructureType }>( + `SELECT map, mapped_type + FROM structure_maps WHERE type = ?`, + ) + .all(type) + const implication_insert = db.prepare( - `INSERT INTO functor_implications ( - id, proof, is_equivalence - ) VALUES (?, ?, ?)`, + `INSERT INTO implications ( + id, type, proof, is_equivalence + ) VALUES (?, ?, ?, ?)`, ) const assumption_insert = db.prepare( - `INSERT INTO functor_implication_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) - - const source_assumption_insert = db.prepare( - `INSERT INTO functor_implication_source_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, + `INSERT INTO assumptions ( + implication_id, property_id, type + ) VALUES (?, ?, ?)`, ) - const target_assumption_insert = db.prepare( - `INSERT INTO functor_implication_target_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, + const conclusion_insert = db.prepare( + `INSERT INTO conclusions ( + implication_id, property_id, type + ) VALUES (?, ?, ?)`, ) - const conclusion_insert = db.prepare( - `INSERT INTO functor_implication_conclusions ( - implication_id, property_id - ) VALUES (?, ?)`, + const mapped_assumption_insert = db.prepare( + `INSERT INTO mapped_assumptions ( + implication_id, map, property_id, type, property_type + ) VALUES (?, ?, ?, ?, ?)`, ) - function insert_implications(implications: FunctorImplicationYaml[]) { + function insert_implications(implications: ImplicationYaml[]) { for (const impl of implications) { - implication_insert.run(impl.id, impl.proof, Number(impl.is_equivalence)) + implication_insert.run(impl.id, type, impl.proof, Number(impl.is_equivalence)) for (const assumption of impl.assumptions) { - assumption_insert.run(impl.id, assumption) + assumption_insert.run(impl.id, assumption, type) } - for (const assumption of impl.source_assumptions) { - source_assumption_insert.run(impl.id, assumption) + for (const conclusion of impl.conclusions) { + conclusion_insert.run(impl.id, conclusion, type) } - for (const assumption of impl.target_assumptions) { - target_assumption_insert.run(impl.id, assumption) - } + if (!impl.mapped_assumptions) continue - for (const conclusion of impl.conclusions) { - conclusion_insert.run(impl.id, conclusion) + for (const { map, mapped_type } of structure_maps) { + const assumptions = impl.mapped_assumptions[map] ?? [] + for (const p of assumptions) { + mapped_assumption_insert.run(impl.id, map, p, type, mapped_type) + } } } } seed_files( db, - 'functor implications', - path.join(data_folder, 'functor-implications'), + `${type} implications`, + path.join(data_folder, folder), insert_implications, ) } - -/** - * Seeds all functors from YAML files. - */ -function seed_functors() { - const functor_insert = db.prepare( - `INSERT INTO functors ( - id, name, notation, source, target, description, nlab_link - ) VALUES (?, ?, ?, ?, ?, ?, ?)`, - ) - - const tag_insert = db.prepare( - `INSERT INTO functor_tag_assignments (functor_id, tag) VALUES (?, ?)`, - ) - - const comment_insert = db.prepare( - `INSERT INTO functor_comments (functor_id, comment) VALUES (?, ?)`, - ) - - const related_insert = db.prepare( - `INSERT INTO related_functors (functor_id, related_functor_id) VALUES (?, ?)`, - ) - - const adjoint_insert = db.prepare( - `INSERT INTO adjoint_functors (left_adjoint, right_adjoint) - VALUES (?, ?) - ON CONFLICT (left_adjoint, right_adjoint) DO NOTHING`, - ) - - const property_assignment_insert = db.prepare( - `INSERT INTO functor_property_assignments ( - functor_id, property_id, is_satisfied, proof, check_redundancy - ) VALUES (?, ?, ?, ?, ?)`, - ) - - function insert_property_assignments( - functor_id: string, - entries: PropertyEntry[], - is_satisfied: 0 | 1 | null, - ) { - for (const entry of entries) { - property_assignment_insert.run( - functor_id, - entry.property, - is_satisfied, - entry.proof, - entry.check_redundancy === false ? 0 : 1, - ) - } - } - - function insert_functor(functor: FunctorYaml) { - functor_insert.run( - functor.id, - functor.name, - functor.notation, - functor.source, - functor.target, - functor.description || null, - functor.nlab_link || null, - ) - - for (const tag of functor.tags) { - tag_insert.run(functor.id, tag) - } - - if (functor.left_adjoint) { - adjoint_insert.run(functor.left_adjoint, functor.id) - } - - for (const comment of functor.comments ?? []) { - comment_insert.run(functor.id, comment) - } - - for (const related of functor.related_functors) { - related_insert.run(functor.id, related) - } - - insert_property_assignments(functor.id, functor.satisfied_properties, 1) - insert_property_assignments(functor.id, functor.unsatisfied_properties, 0) - insert_property_assignments( - functor.id, - functor.undecidable_properties ?? [], - null, - ) - } - - seed_files(db, 'functors', path.join(data_folder, 'functors'), insert_functor) -} diff --git a/databases/catdat/scripts/setup.ts b/databases/catdat/scripts/setup.ts index 0e2262105..f70c93a2d 100644 --- a/databases/catdat/scripts/setup.ts +++ b/databases/catdat/scripts/setup.ts @@ -1,6 +1,6 @@ import fs from 'node:fs' import path from 'node:path' -import { get_client } from './utils/helpers' +import { get_client } from './utils/db' import { create_schema_hash, write_schema_hash } from './utils/schema' const schema_folder = path.resolve('databases', 'catdat', 'schema') diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index 3b802a642..51941449a 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -11,8 +11,9 @@ import forget_vector_expected from './expected-data/forget_vector.json' import id_Set_expected from './expected-data/id_Set.json' import decided_categories from './expected-data/decided-categories.json' import decided_functors from './expected-data/decided-functors.json' -import { capitalize, get_client } from './utils/helpers' -import { StructureType } from './config' +import { capitalize } from './utils/helpers' +import { get_client } from './utils/db' +import { PLURALS, StructureType } from './config' const db = get_client() @@ -24,8 +25,8 @@ execute_tests() function execute_tests() { try { console.info('\n--- Test categories ---') - test_mutual_category_duals() - test_properties_of_trivial_category() + test_mutual_structure_duals('category') + test_positivity('1', 'category') test_mutual_property_duals('category') test_decided_structures(decided_categories, 'category') test_properties_of_selected_structures( @@ -34,6 +35,7 @@ function execute_tests() { ) console.info('\n--- Test functors ---') + test_positivity('id_Set', 'functor') test_mutual_property_duals('functor') test_decided_structures(decided_functors, 'functor') test_properties_of_selected_structures( @@ -51,51 +53,55 @@ function execute_tests() { } /** - * Tests for all categories C,D that if C is dual to D, then D is dual to C. + * Tests for all structures of a given type C,D that if + * C is dual to D, then D is dual to C. */ -function test_mutual_category_duals() { +function test_mutual_structure_duals(type: StructureType) { const dict: Record = {} - const categories = db - .prepare< - never[], - { id: string; dual_category_id: string | null } - >('SELECT id, dual_category_id FROM categories') - .all() + const structures_with_duals = db + .prepare<[StructureType], { id: string; dual: string | null }>( + `SELECT id, dual_structure_id AS dual + FROM structures WHERE type = ?`, + ) + .all(type) - for (const { id, dual_category_id } of categories) { - dict[id] = dual_category_id + for (const { id, dual } of structures_with_duals) { + dict[id] = dual } for (const id in dict) { const dual = dict[id] if (dual && dict[dual] !== id) { - throw new Error(`❌ Found non-mutual category duality: ${id}, ${dual}`) + throw new Error(`❌ Found non-mutual ${type} duality: ${id}, ${dual}`) } } - console.info(`✅ Categories are mutually dual`) + console.info(`✅ ${capitalize(PLURALS[type])} are mutually dual`) } /** - * Tests that the trivial category has no unsatisfied property. + * Tests that a specified structure has no unsatisfied property. * This enforces that all properties in the database are "positive". */ -function test_properties_of_trivial_category() { - const rows = db - .prepare( - `SELECT property_id FROM category_property_assignments - WHERE category_id = '1' AND is_satisfied = FALSE`, +function test_positivity(structure_id: string, type: StructureType) { + const unsatisfied_props = db + .prepare<[StructureType, string], { property_id: string }>( + `SELECT property_id FROM property_assignments + WHERE + type = ? AND + structure_id = ? AND + is_satisfied = FALSE`, ) - .all() + .all(type, structure_id) - if (rows.length > 0) { + if (unsatisfied_props.length > 0) { throw new Error( - `❌ The trivial category has ${rows.length} unsatisfied properties, but it should have 0.`, + `❌ The ${type} ${structure_id} has ${unsatisfied_props.length} unsatisfied properties, but it should have 0.`, ) } - console.info(`✅ The trivial category has no unsatisfied properties`) + console.info(`✅ The ${type} ${structure_id} has no unsatisfied properties`) } /** @@ -107,10 +113,10 @@ function test_mutual_property_duals(type: StructureType) { const properties = db .prepare< - never[], + [StructureType], { id: string; dual_property_id: string | null } - >(`SELECT id, dual_property_id FROM ${type}_properties`) - .all() + >(`SELECT id, dual_property_id FROM properties WHERE type = ?`) + .all(type) for (const { id, dual_property_id } of properties) { dict[id] = dual_property_id @@ -131,16 +137,19 @@ function test_mutual_property_duals(type: StructureType) { * been decided. If this test fails, property assignments or implications are missing. */ function test_decided_structures(structure_ids: string[], type: StructureType) { - const unknown_query = db.prepare<[string], { id: string }>( - `SELECT p.id FROM ${type}_properties p WHERE NOT EXISTS - (SELECT 1 FROM ${type}_property_assignments - WHERE ${type}_id = ? AND property_id = p.id + const unknown_query = db.prepare< + [StructureType, StructureType, string], + { id: string } + >( + `SELECT p.id FROM properties p WHERE type = ? AND NOT EXISTS + (SELECT 1 FROM property_assignments + WHERE type = ? AND structure_id = ? AND property_id = p.id ) `, ) for (const structure_id of structure_ids) { - const res = unknown_query.all(structure_id) + const res = unknown_query.all(type, type, structure_id) const unknown_properties = res.map((row) => row.id) if (unknown_properties.length > 0) { @@ -164,15 +173,15 @@ function test_properties_of_selected_structures( type: StructureType, ) { const property_query = db.prepare< - [string], + [StructureType, string], { property_id: string; is_satisfied: 0 | 1 } >( - `SELECT property_id, is_satisfied FROM ${type}_property_assignments - WHERE ${type}_id = ? AND is_satisfied IS NOT NULL`, + `SELECT property_id, is_satisfied FROM property_assignments + WHERE type = ? AND structure_id = ? AND is_satisfied IS NOT NULL`, ) for (const structure_id in expected) { - const properties = property_query.all(structure_id) + const properties = property_query.all(type, structure_id) for (const { property_id, is_satisfied } of properties) { const ok = Boolean(is_satisfied) === expected[structure_id][property_id] diff --git a/databases/catdat/scripts/utils/categories.ts b/databases/catdat/scripts/utils/categories.ts deleted file mode 100644 index 4b00a8f41..000000000 --- a/databases/catdat/scripts/utils/categories.ts +++ /dev/null @@ -1,77 +0,0 @@ -import { type Database } from 'better-sqlite3' -import { parse_json_set } from './helpers' - -type CategoryMeta = { - id: string - name: string - dual: string | null -} - -export type NormalizedCategoryImplication = { - id: string - assumptions: Set - conclusion: string -} - -/** - * Returns the list of categories saved in the database. - */ -export function get_categories(db: Database) { - return db - .prepare( - `SELECT id, name, dual_category_id AS dual - FROM categories ORDER BY lower(name)`, - ) - .all() -} - -/** - * Implications have the form - * P_1 + ... + P_n ===> Q_1 + ... + Q_m - * or - * P_1 + ... + P_n <===> Q_1 + ... + Q_m. - * This function decomposes them into normalized implications, - * which have the form - * P_1 + ... + P_n ===> Q. - */ -export function get_normalized_category_implications( - db: Database, -): NormalizedCategoryImplication[] { - const all_implications_db = db - .prepare< - never[], - { - id: string - assumptions: string - conclusions: string - is_equivalence: 0 | 1 - } - >( - `SELECT id, assumptions, conclusions, is_equivalence - FROM category_implications_view`, - ) - .all() - - const implications: NormalizedCategoryImplication[] = [] - - for (const impl of all_implications_db) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - - for (const conclusion of conclusions) { - implications.push({ id: impl.id, assumptions, conclusion }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption, - }) - } - } - } - - return implications -} diff --git a/databases/catdat/scripts/utils/db.ts b/databases/catdat/scripts/utils/db.ts new file mode 100644 index 000000000..a2b477874 --- /dev/null +++ b/databases/catdat/scripts/utils/db.ts @@ -0,0 +1,9 @@ +import Database from 'better-sqlite3' +import path from 'node:path' + +export function get_client() { + const db_path = path.resolve('databases', 'catdat', 'catdat.db') + const db = new Database(db_path, { readonly: false }) + db.pragma('foreign_keys = ON') + return db +} diff --git a/databases/catdat/scripts/utils/deduction.ts b/databases/catdat/scripts/utils/deduction.ts deleted file mode 100644 index 0bd662327..000000000 --- a/databases/catdat/scripts/utils/deduction.ts +++ /dev/null @@ -1,194 +0,0 @@ -import { type Database } from 'better-sqlite3' -import { get_categories, get_normalized_category_implications } from './categories' -import { get_functors, get_normalized_functor_implications } from './functors' -import { StructureType } from '../config' - -/** - * A structure is a category or a functor. - */ -export type StructureMeta = { - id: string - name: string - dual?: string | null - // used for source and target properties of a functor - associated_satisfied_properties?: Record> -} - -export type NormalizedImplication = { - id: string - assumptions: Set - conclusion: string - // used for source and target assumptions of a functor in an implication - associated_assumptions?: Record> -} - -export type PropertyMeta = { - id: string - dual: string | null - relation: string - conditional: string -} - -/** - * Returns the list of stored categorical structures of a given type. - */ -export function get_structures(db: Database, type: StructureType): StructureMeta[] { - if (type === 'category') return get_categories(db) - if (type === 'functor') return get_functors(db) - throw new Error('Unsupported type') -} - -/** - * Returns the list of normalized implications saved in the database of a given type. - */ -export function get_normalized_implications( - db: Database, - type: StructureType, -): NormalizedImplication[] { - if (type === 'category') return get_normalized_category_implications(db) - if (type === 'functor') return get_normalized_functor_implications(db) - throw new Error('Unsupported type') -} - -/** - * Returns a dictionary of properties saved in the database. - */ -export function get_properties_dict(db: Database, type: StructureType) { - const properties = db - .prepare( - `SELECT - p.id, p.dual_property_id AS dual, p.relation, - r.conditional - FROM ${type}_properties p - INNER JOIN relations r ON r.relation = p.relation - ORDER BY lower(p.id)`, - ) - .all() - - const dict: Record = {} - - for (const p of properties) dict[p.id] = p - - return dict -} - -/** - * Returns a dictionary with all assigned properties of a list of structures - * (categories or functors), grouped by id and - * value (satisfied / unsatisfied / undecidable). - */ -export function get_property_assignments( - db: Database, - structures: { id: string }[], - type: StructureType, -) { - const rows = db - .prepare< - never[], - { - property_id: string - structure_id: string - is_satisfied: 0 | 1 | null - } - >( - `SELECT - property_id, - ${type}_id AS structure_id, - is_satisfied - FROM ${type}_property_assignments`, - ) - .all() - - const grouped: Record< - string, - { satisfied: Set; unsatisfied: Set; undecidable: Set } - > = {} - - for (const structure of structures) { - grouped[structure.id] = { - satisfied: new Set(), - unsatisfied: new Set(), - undecidable: new Set(), - } - } - - for (const row of rows) { - const { property_id, structure_id, is_satisfied } = row - let group_key: 'satisfied' | 'unsatisfied' | 'undecidable' - if (is_satisfied === 1) { - group_key = 'satisfied' - } else if (is_satisfied === 0) { - group_key = 'unsatisfied' - } else { - group_key = 'undecidable' - } - grouped[structure_id][group_key].add(property_id) - } - - return grouped -} - -/** - * Returns a dictionary with all assigned properties of structures, - * grouped by structure, value (satisfied / unsatisfied), and deduced status. - * We exclude undecidable properties here. - */ -export function get_property_assignments_by_deduction( - db: Database, - structures: { id: string }[], - type: StructureType, -) { - const rows = db - .prepare< - never[], - { - property_id: string - structure_id: string - is_satisfied: 0 | 1 - is_deduced: 0 | 1 - } - >( - `SELECT - property_id, - ${type}_id AS structure_id, - is_satisfied, - is_deduced - FROM ${type}_property_assignments - WHERE is_satisfied IS NOT NULL`, - ) - .all() - - const grouped: Record< - string, - { - satisfied: { non_deduced: Set; deduced: Set } - unsatisfied: { non_deduced: Set; deduced: Set } - } - > = {} - - for (const structure of structures) { - grouped[structure.id] = { - satisfied: { non_deduced: new Set(), deduced: new Set() }, - unsatisfied: { non_deduced: new Set(), deduced: new Set() }, - } - } - - for (const row of rows) { - const { property_id, structure_id, is_satisfied, is_deduced } = row - grouped[structure_id][is_satisfied ? 'satisfied' : 'unsatisfied'][ - is_deduced ? 'deduced' : 'non_deduced' - ].add(property_id) - } - - return grouped -} - -/** - * Checks if an structure is a dual, but not the - * original structure to prevent circular reasoning. - */ -export function is_dual_structure( - structure: StructureMeta, -): structure is StructureMeta & { dual: string } { - return Boolean(structure.dual) && structure.name.toLowerCase().startsWith('dual') -} diff --git a/databases/catdat/scripts/utils/functors.ts b/databases/catdat/scripts/utils/functors.ts deleted file mode 100644 index b9180d34f..000000000 --- a/databases/catdat/scripts/utils/functors.ts +++ /dev/null @@ -1,141 +0,0 @@ -import { type Database } from 'better-sqlite3' -import { parse_json_set } from './helpers' - -type FunctorMeta = { - id: string - name: string - associated_satisfied_properties: { - source: Set - target: Set - } -} - -type NormalizedFunctorImplication = { - id: string - assumptions: Set - conclusion: string - associated_assumptions: { - source: Set - target: Set - } -} - -/** - * Returns the list of functors saved in the database along with - * the satisfied properties of their source and target category. - */ -export function get_functors(db: Database): FunctorMeta[] { - const rows = db - .prepare< - never[], - { - id: string - name: string - source: string - target: string - source_props: string - target_props: string - } - >( - `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)`, - ) - .all() - - return rows.map((row) => ({ - id: row.id, - name: row.name, - associated_satisfied_properties: { - source: parse_json_set(row.source_props), - target: parse_json_set(row.target_props), - }, - })) -} - -/** - * Implications have the form - * P_1 + ... + P_n ===> Q_1 + ... + Q_m - * or - * P_1 + ... + P_n <===> Q_1 + ... + Q_m. - * This function decomposes them into normalized implications, - * which have the form - * P_1 + ... + P_n ===> Q. - */ -export function get_normalized_functor_implications( - db: Database, -): NormalizedFunctorImplication[] { - const all_implications_db = db - .prepare< - never[], - { - id: string - assumptions: string - source_assumptions: string - target_assumptions: string - conclusions: string - is_equivalence: 0 | 1 - } - >( - `SELECT - id, assumptions, source_assumptions, target_assumptions, - conclusions, is_equivalence - FROM functor_implications_view`, - ) - .all() - - const implications: NormalizedFunctorImplication[] = [] - - for (const impl of all_implications_db) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - const source_assumptions = parse_json_set(impl.source_assumptions) - const target_assumptions = parse_json_set(impl.target_assumptions) - - for (const conclusion of conclusions) { - implications.push({ - id: impl.id, - assumptions, - conclusion, - associated_assumptions: { - source: source_assumptions, - target: target_assumptions, - }, - }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption, - associated_assumptions: { - source: source_assumptions, - target: target_assumptions, - }, - }) - } - } - } - - return implications -} diff --git a/databases/catdat/scripts/utils/helpers.ts b/databases/catdat/scripts/utils/helpers.ts index b5c347252..7d66d9e28 100644 --- a/databases/catdat/scripts/utils/helpers.ts +++ b/databases/catdat/scripts/utils/helpers.ts @@ -1,8 +1,3 @@ -import Database, { type Database as DatabaseType } from 'better-sqlite3' -import path from 'node:path' -import fs from 'node:fs' -import YAML from 'yaml' - export function are_equal_sets(a: Set, b: Set) { return a.size === b.size && [...a].every((el) => b.has(el)) } @@ -22,72 +17,11 @@ export function parse_json_set(json: string): Set { return new Set(JSON.parse(json)) } -export function get_client() { - const db_path = path.resolve('databases', 'catdat', 'catdat.db') - const db = new Database(db_path, { readonly: false }) - db.pragma('foreign_keys = ON') - return db -} - -function read_yaml_file(...parts: string[]): T { - const content = fs.readFileSync(path.join(...parts), 'utf8') - return YAML.parse(content) as T -} - -function get_yaml_files(folder: string) { - return fs - .readdirSync(folder) - .filter((file) => file.endsWith('.yaml')) - .sort() -} - -export function seed_file( - db: DatabaseType, - label: string, - file: string, - insert: (item: T) => void, -) { - console.info(`\nSeed ${label} ...`) - const item = read_yaml_file(file) - - const tx = db.transaction(() => { - db.pragma('defer_foreign_keys = ON') - insert(item) - }) - - try { - tx() - } catch (err) { - console.error(`Error seeding ${label}:`, err) - process.exit(1) - } -} - -export function seed_files( - db: DatabaseType, - label: string, - folder: string, - insert: (item: T) => void, -) { - console.info(`\nSeed ${label} ...`) - - const files = get_yaml_files(folder) - - const tx = db.transaction(() => { - db.pragma('defer_foreign_keys = ON') - - for (const file of files) { - console.info(`Seed: ${file}`) - - const item = read_yaml_file(folder, file) - insert(item) - } - }) - - try { - tx() - } catch (err) { - console.error(`Error seeding ${label}:`, err) - process.exit(1) +export function parse_nested_json_set(json: string): Partial>> { + const obj = JSON.parse(json) + const result: Partial>> = {} + for (const key in obj) { + result[key] = parse_json_set(obj[key]) } + return result } diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index 1ca4613e2..f0388769b 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/databases/catdat/scripts/utils/implications.ts @@ -1,7 +1,90 @@ import { type Database } from 'better-sqlite3' -import type { NormalizedImplication, PropertyMeta } from './deduction' -import { are_equal_sets, parse_json_set } from './helpers' +import type { PropertyMeta } from './properties' import { StructureType } from '../config' +import { parse_nested_json_set, parse_json_set } from './helpers' + +export type NormalizedImplication = { + id: string + assumptions: Set + conclusion: string + mapped_assumptions?: Partial>> +} + +/** + * Implications have the form + * P_1 + ... + P_n ===> Q_1 + ... + Q_m + * or + * P_1 + ... + P_n <===> Q_1 + ... + Q_m. + * This function decomposes them into normalized implications, + * which have the form + * P_1 + ... + P_n ===> Q. + */ +export function get_normalized_implications( + db: Database, + type: StructureType, +): NormalizedImplication[] { + const implications_db = db + .prepare< + [StructureType], + { + id: string + is_equivalence: 0 | 1 + assumptions: string + conclusions: string + mapped_assumptions: string + } + >( + `SELECT + id, + is_equivalence, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view i + WHERE i.type = ?`, + ) + .all(type) + + const implications: NormalizedImplication[] = [] + + for (const impl of implications_db) { + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) + const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) + + for (const conclusion of conclusions) { + const implication: NormalizedImplication = { + id: impl.id, + assumptions, + conclusion, + } + + if (Object.keys(mapped_assumptions).length > 0) { + implication.mapped_assumptions = mapped_assumptions + } + + implications.push(implication) + } + + if (impl.is_equivalence) { + for (const assumption of assumptions) { + const implication: NormalizedImplication = { + id: impl.id, + assumptions: conclusions, + conclusion: assumption, + } + + if (Object.keys(mapped_assumptions).length > 0) { + implication.mapped_assumptions = mapped_assumptions + } + + implications.push(implication) + } + } + } + + return implications +} function get_assumption_string( implication: NormalizedImplication, @@ -13,7 +96,7 @@ function get_assumption_string( return Array.from(assumptions) .map( (assumption) => - `${properties_dict[assumption][conditional ? 'conditional' : 'relation']} ${assumption}`, + `${properties_dict[assumption][conditional ? 'conditional_relation' : 'relation']} ${assumption}`, ) .join(' and ') } @@ -25,7 +108,7 @@ function get_conclusion_string( ): string { const { conclusion } = implication - return `${properties_dict[conclusion][conditional ? 'conditional' : 'relation']} ${conclusion}` + return `${properties_dict[conclusion][conditional ? 'conditional_relation' : 'relation']} ${conclusion}` } export function get_proof_string( @@ -53,57 +136,11 @@ export function get_contradiction_string( const ref = `by this result` - const contra = `Assume for contradiction that it ${properties_dict[property].relation} ${property}` + const relation = properties_dict[property].relation + + const contra = `Assume for contradiction that it ${relation} ${property}` return has_multiple_assumptions ? `${contra}. Then it ${assumption_string}, so it ${conclusion_string} (${ref}) – contradiction.` : `${contra}. Then it ${conclusion_string} (${ref}) – contradiction.` } - -/** - * Clears all deduced implications. This is done before the deduction starts. - */ -export function clear_deduced_implications(db: Database, type: StructureType) { - db.prepare(`DELETE FROM ${type}_implications WHERE is_deduced = TRUE`).run() -} - -type ImplicationWithDualProperties = { - assumptions: string - conclusions: string - dual_assumptions: string - dual_conclusions: string - dual_source_assumptions?: string - dual_target_assumptions?: string -} - -/** - * Checks if an implication can be dualized (i.e. if all the involved properties - * have a dual) and if the dual is different from it. - */ -export function is_dualizable(impl: ImplicationWithDualProperties): boolean { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - const dual_assumptions = parse_json_set(impl.dual_assumptions) - const dual_conclusions = parse_json_set(impl.dual_conclusions) - - if (dual_assumptions.has(null) || dual_conclusions.has(null)) return false - - if (impl.dual_source_assumptions) { - const dual_source_assumptions = parse_json_set( - impl.dual_source_assumptions, - ) - if (dual_source_assumptions.has(null)) return false - } - - if (impl.dual_target_assumptions) { - const dual_target_assumptions = parse_json_set( - impl.dual_target_assumptions, - ) - if (dual_target_assumptions.has(null)) return false - } - - return !( - are_equal_sets(assumptions, dual_assumptions) && - are_equal_sets(conclusions, dual_conclusions) - ) -} diff --git a/databases/catdat/scripts/utils/properties.ts b/databases/catdat/scripts/utils/properties.ts new file mode 100644 index 000000000..b9a1d5b07 --- /dev/null +++ b/databases/catdat/scripts/utils/properties.ts @@ -0,0 +1,156 @@ +import { type Database } from 'better-sqlite3' +import type { StructureType } from '../config' + +/** + * Property of a categorical structure + */ +export type PropertyMeta = { + id: string + dual: string | null + relation: string // e.g. "is" + conditional_relation: string // e.g. "would be" +} + +/** + * Returns a dictionary of properties saved in the database. + */ +export function get_properties_dict(db: Database, type: StructureType) { + const properties = db + .prepare<[StructureType], PropertyMeta>( + `SELECT + p.id, + p.dual_property_id AS dual, + p.relation, + r.conditional AS conditional_relation + FROM properties p + INNER JOIN relations r ON r.relation = p.relation + WHERE type = ? + ORDER BY lower(p.id)`, + ) + .all(type) + + const dict: Record = {} + + for (const p of properties) dict[p.id] = p + + return dict +} + +/** + * Returns a dictionary with all assigned properties of a list of structures + * (categories or functors), grouped by id and + * value (satisfied / unsatisfied / undecidable). + */ +export function get_property_assignments( + db: Database, + structures: { id: string }[], + type: StructureType, +) { + const assignments = db + .prepare< + [StructureType], + { + property_id: string + structure_id: string + is_satisfied: 0 | 1 | null + } + >( + `SELECT + property_id, + structure_id, + is_satisfied + FROM property_assignments + WHERE type = ?`, + ) + .all(type) + + const dict = Object.fromEntries( + structures.map((s) => [ + s.id, + { + satisfied: new Set(), + unsatisfied: new Set(), + undecidable: new Set(), + }, + ]), + ) + + for (const assignment of assignments) { + const { property_id, structure_id, is_satisfied } = assignment + const key = get_assignment_key(is_satisfied) + dict[structure_id][key].add(property_id) + } + + return dict +} + +/** + * Returns the key in the assignment dictionary + */ +function get_assignment_key(is_satisfied: 0 | 1 | null) { + if (is_satisfied === 1) { + return 'satisfied' + } else if (is_satisfied === 0) { + return 'unsatisfied' + } else { + return 'undecidable' + } +} + +/** + * Returns a dictionary with all assigned properties of structures, + * grouped by structure, value (satisfied / unsatisfied), and deduced status. + * We exclude undecidable properties here. + */ +export function get_property_assignments_by_deduction( + db: Database, + structures: { id: string }[], + type: StructureType, +) { + const assignments = db + .prepare< + [StructureType], + { + property_id: string + structure_id: string + is_satisfied: 0 | 1 + is_deduced: 0 | 1 + } + >( + `SELECT + property_id, + structure_id, + is_satisfied, + is_deduced + FROM property_assignments + WHERE + type = ? + AND is_satisfied IS NOT NULL`, + ) + .all(type) + + const dict = Object.fromEntries( + structures.map((s) => [ + s.id, + { + satisfied: { + non_deduced: new Set(), + deduced: new Set(), + }, + unsatisfied: { + non_deduced: new Set(), + deduced: new Set(), + }, + }, + ]), + ) + + for (const assignment of assignments) { + const { property_id, structure_id, is_satisfied, is_deduced } = assignment + const value_key = is_satisfied ? 'satisfied' : 'unsatisfied' + const status_key = is_deduced ? 'deduced' : 'non_deduced' + dict[structure_id][value_key][status_key].add(property_id) + } + + return dict +} diff --git a/databases/catdat/scripts/utils/seed.helpers.ts b/databases/catdat/scripts/utils/seed.helpers.ts new file mode 100644 index 000000000..5cfb850f3 --- /dev/null +++ b/databases/catdat/scripts/utils/seed.helpers.ts @@ -0,0 +1,67 @@ +import type { Database } from 'better-sqlite3' +import path from 'node:path' +import fs from 'node:fs' +import YAML from 'yaml' + +function read_yaml_file(...parts: string[]): T { + const content = fs.readFileSync(path.join(...parts), 'utf8') + return YAML.parse(content) as T +} + +function get_yaml_files(folder: string) { + return fs + .readdirSync(folder) + .filter((file) => file.endsWith('.yaml')) + .sort() +} + +export function seed_file( + db: Database, + label: string, + file: string, + insert: (item: T) => void, +) { + console.info(`\nSeed ${label} ...`) + const item = read_yaml_file(file) + + const tx = db.transaction(() => { + db.pragma('defer_foreign_keys = ON') + insert(item) + }) + + try { + tx() + } catch (err) { + console.error(`Error seeding ${label}:`, err) + process.exit(1) + } +} + +export function seed_files( + db: Database, + label: string, + folder: string, + insert: (item: T) => void, +) { + console.info(`\nSeed ${label} ...`) + + const files = get_yaml_files(folder) + + const tx = db.transaction(() => { + db.pragma('defer_foreign_keys = ON') + + for (const file of files) { + console.info(`Seed: ${file}`) + + const item = read_yaml_file(folder, file) + insert(item) + } + }) + + try { + tx() + } catch (err) { + console.error(`Error seeding ${label}:`, err) + process.exit(1) + } +} diff --git a/databases/catdat/scripts/seed.types.ts b/databases/catdat/scripts/utils/seed.types.ts similarity index 58% rename from databases/catdat/scripts/seed.types.ts rename to databases/catdat/scripts/utils/seed.types.ts index bfe7e29ce..01adf4d30 100644 --- a/databases/catdat/scripts/seed.types.ts +++ b/databases/catdat/scripts/utils/seed.types.ts @@ -16,25 +16,6 @@ export type ConfigYaml = { }[] } -export type CategoryYaml = { - id: string - name: string - notation: string - objects: string - morphisms: string - description: string | null - nlab_link: string | null - dual_category?: string | null - tags: string[] - related_categories: string[] - satisfied_properties: PropertyEntry[] - unsatisfied_properties: PropertyEntry[] - undecidable_properties?: PropertyEntry[] - special_objects: Record - special_morphisms: Record - comments?: string[] -} - export type PropertyEntry = { property: string proof: string @@ -50,59 +31,53 @@ type MorphismEntry = { proof: string } -export type CategoryPropertyYaml = { +export type StructureYaml = { id: string - relation: string - description: string - nlab_link?: string | null - dual_property?: string | null - invariant_under_equivalences: boolean - related_properties: string[] + name: string + notation: string + description?: string | null + nlab_link?: string + left_adjoint?: string + tags: string[] + related_categories?: string[] // TODO: improve this + related_functors?: string[] + dual_category?: string // TODO: improve this + dual_functor?: string + satisfied_properties: PropertyEntry[] + unsatisfied_properties: PropertyEntry[] + undecidable_properties?: PropertyEntry[] + comments?: string[] } -export type CategoryImplicationYaml = { - id: string - assumptions: string[] - conclusions: string[] - proof: string - is_equivalence: boolean +export type CategoryYaml = StructureYaml & { + objects: string + morphisms: string + dual_category?: string | null + special_objects: Record + special_morphisms: Record } -export type FunctorImplicationYaml = { - id: string - assumptions: string[] - source_assumptions: string[] - target_assumptions: string[] - conclusions: string[] - proof: string - is_equivalence: boolean +export type FunctorYaml = StructureYaml & { + source: string + target: string + left_adjoint?: string } -export type FunctorPropertyYaml = { +export type PropertyYaml = { id: string relation: string description: string - required_source?: string - required_target?: string nlab_link?: string | null dual_property?: string | null invariant_under_equivalences: boolean related_properties: string[] } -export type FunctorYaml = { +export type ImplicationYaml = { id: string - name: string - notation: string - source: string - target: string - description?: string | null - nlab_link?: string - left_adjoint?: string - tags: string[] - related_functors: string[] - satisfied_properties: PropertyEntry[] - unsatisfied_properties: PropertyEntry[] - undecidable_properties?: PropertyEntry[] - comments?: string[] + assumptions: string[] + conclusions: string[] + mapped_assumptions?: Partial> + proof: string + is_equivalence: boolean } diff --git a/databases/catdat/scripts/utils/structures.ts b/databases/catdat/scripts/utils/structures.ts new file mode 100644 index 000000000..0f5e64090 --- /dev/null +++ b/databases/catdat/scripts/utils/structures.ts @@ -0,0 +1,105 @@ +import { type Database } from 'better-sqlite3' +import { StructureType } from '../config' +import { parse_json_set } from './helpers' + +/** + * Type for various types of categorical structures (category, functor, ...) + */ +export type StructureMeta = { + id: string + name: string + dual?: string | null + associated_satisfied_properties?: Record> +} + +/** + * Returns the list of stored categorical structures of a given type. + */ +export function get_structures(db: Database, type: StructureType): StructureMeta[] { + if (type === 'category') return get_categories(db) + if (type === 'functor') return get_functors(db) + throw new Error('Unsupported type') +} + +/** + * Returns the list of categories saved in the database. + */ +function get_categories(db: Database) { + return db + .prepare< + never[], + { + id: string + name: string + dual: string | null + } + >( + `SELECT + c.id, + s.name, + s.dual_structure_id AS dual + FROM categories c + INNER JOIN structures s ON s.id = c.id + ORDER BY lower(s.name)`, + ) + .all() +} + +/** + * Returns the list of functors saved in the database along with + * the satisfied properties of their source and target category. + */ +function get_functors(db: Database) { + const rows = db + .prepare< + never[], + { + id: string + name: string + source_props: string + target_props: string + } + >( + `SELECT + f.id, + s.name, + ( + SELECT json_group_array(property_id) + FROM property_assignments + WHERE + structure_id = f.source + AND is_satisfied = TRUE + + ) AS source_props, + ( + SELECT json_group_array(property_id) + FROM property_assignments + WHERE + structure_id = f.target + AND is_satisfied = TRUE + ) AS target_props + FROM functors f + INNER JOIN structures s ON s.id = f.id + ORDER BY lower(s.name)`, + ) + .all() + + return rows.map((functor) => ({ + id: functor.id, + name: functor.name, + associated_satisfied_properties: { + source: parse_json_set(functor.source_props), + target: parse_json_set(functor.target_props), + }, + })) +} + +/** + * Checks if a structure is a dual, but not the + * original structure to prevent circular reasoning. + */ +export function is_dual_structure( + structure: StructureMeta, +): structure is StructureMeta & { dual: string } { + return Boolean(structure.dual) && structure.name.toLowerCase().startsWith('dual') +} diff --git a/src/components/CategoryDescription.svelte b/src/components/CategoryDescription.svelte deleted file mode 100644 index 68ffd1bc9..000000000 --- a/src/components/CategoryDescription.svelte +++ /dev/null @@ -1,70 +0,0 @@ - - -
    -
      -
    • - notation: - {@html category.notation} -
      • - -
    • - objects: - {@html category.objects} -
      • - -
    • - morphisms: - {@html category.morphisms} -
      • - - {#if related_categories.length} -
    • - Related categories: - {#each related_categories as { id, name, notation }, i} - - {@html notation} - {#if i < related_categories.length - 1} - ,  - {/if} - {/each} -
      • - {/if} - - {#if category.nlab_link} -
    • - nLab Link -
      • - {/if} - - {#if category.dual_category_id} -
    • - Dual category: - - {@html category.dual_category_notation} - -
      • - {/if} -
    - - {#if category.description} -

    {@html category.description}

    - {/if} -
    - - diff --git a/src/components/FunctorDescription.svelte b/src/components/FunctorDescription.svelte deleted file mode 100644 index e5613456d..000000000 --- a/src/components/FunctorDescription.svelte +++ /dev/null @@ -1,76 +0,0 @@ - - -
    - - -

    {@html functor.description}

    -
    - - diff --git a/src/components/ImplicationItem.svelte b/src/components/ImplicationItem.svelte index 4d9c55e8e..542e3dbd9 100644 --- a/src/components/ImplicationItem.svelte +++ b/src/components/ImplicationItem.svelte @@ -18,8 +18,7 @@ let { type, implication, highlighted_property }: Props = $props() let has_additional_assumptions = $derived( - Boolean(implication.source_assumptions?.length) || - Boolean(implication.target_assumptions?.length), + Object.values(implication.mapped_assumptions).some((list) => list?.length), ) diff --git a/src/components/StructureDetailPage.svelte b/src/components/StructureDetailPage.svelte new file mode 100644 index 000000000..c555f7236 --- /dev/null +++ b/src/components/StructureDetailPage.svelte @@ -0,0 +1,127 @@ + + + + +

    {structure.name}

    + + + +
    +
      +
    • + notation: + {@html structure.notation} +
      • + + {@render definition?.()} + + {#if related_structures.length} +
    • + Related {PLURALS[type]}: + {#each related_structures as { id, name, notation }, i} + + {@html notation} + {#if i < related_structures.length - 1} + ,  + {/if} + {/each} +
      • + {/if} + + {#if structure.nlab_link} +
    • + nLab Link +
      • + {/if} + + {#if structure.dual_structure_id} +
    • + Dual {type}: + + {@html structure.dual_structure_notation} + +
      • + {/if} +
    + + {#if structure.description} +

    {@html structure.description}

    + {/if} +
    + + + +{@render specials?.()} + + + + + + + + diff --git a/src/lib/commons/structures.ts b/src/lib/commons/structures.ts index 125843088..72e797083 100644 --- a/src/lib/commons/structures.ts +++ b/src/lib/commons/structures.ts @@ -6,3 +6,12 @@ export const PLURALS = { category: 'categories', functor: 'functors', } + +export function get_selected_type(pathname: string): StructureType { + for (const type of STRUCTURES) { + const matches = + pathname.startsWith(`/${type}`) || pathname.startsWith(`/${PLURALS[type]}`) + if (matches) return type + } + return 'category' +} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index cd8071169..af2ebcb2e 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -13,19 +13,39 @@ export type StructureShort = { export type RelatedStructure = StructureShort & { notation: string } -export type CategoryDisplay = { +export type StructureDisplay = { id: string name: string notation: string - objects: string - morphisms: string description: string | null nlab_link: string | null - dual_category_id: string | null - dual_category_name: string | null - dual_category_notation: string | null + dual_structure_id: string | null + dual_structure_name: string | null + dual_structure_notation: string | null +} + +export type CategorySpecificDisplay = { + objects: string + morphisms: string +} + +export type FunctorSpecificDisplay = { + source: string + source_name: string + source_notation: string + target: string + target_name: string + target_notation: string + left_adjoint: string | null + left_adjoint_name: string | null + left_adjoint_notation: string | null + right_adjoint: string | null + right_adjoint_name: string | null + right_adjoint_notation: string | null } +export type MappedTypes = Record + export type TagObject = { tag: string } export type CommentObject = { id: number; comment: string } @@ -78,20 +98,6 @@ export type SpecialMorphism = { proof: string } -export type FunctorDisplay = { - id: string - name: string - notation: string - source: string - target: string - source_name: string - target_name: string - source_notation: string - target_notation: string - description: string - nlab_link: string | null -} - export type ImplicationDB = { id: string is_equivalence: 0 | 1 @@ -100,8 +106,7 @@ export type ImplicationDB = { proof: string assumptions: string conclusions: string - source_assumptions?: string // for functors - target_assumptions?: string // for functors + mapped_assumptions: string } export type ImplicationDisplay = Replace< @@ -111,13 +116,17 @@ export type ImplicationDisplay = Replace< is_deduced: boolean assumptions: string[] conclusions: string[] - source_assumptions?: string[] - target_assumptions?: string[] + mapped_assumptions: Partial> } > +export type NormalizedImplication = { + id: string + assumptions: Set + conclusion: string +} + export type SearchResults = { - type: StructureType contradiction: string[] | null satisfied_properties: string[] unsatisfied_properties: string[] @@ -128,7 +137,6 @@ export type SearchResults = { } export type ComparisonResult = { - type: StructureType structures: RelatedStructure[] comparison_table: string[][] } diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index f548eab4b..4f31a8bf4 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -1,12 +1,7 @@ -import { query } from '$lib/server/db.catdat' import { is_subset } from './utils' import type { SqliteError } from 'better-sqlite3' -import { - get_normalized_implications, - stringify_implication, - type NormalizedImplication, -} from './implications' -import type { StructureType } from '$lib/commons/types' +import type { NormalizedImplication, StructureType } from '$lib/commons/types' +import { get_normalized_implications } from './fetchers/implications' // TODO: If possible, remove the code duplication with deduction and redundancy scripts. @@ -33,7 +28,7 @@ export function get_contradiction( return { contradiction, err: null } } -function contradiction_worker( +export function contradiction_worker( satisfied_properties: Set, unsatisfied_properties: Set, implications: NormalizedImplication[], @@ -109,62 +104,6 @@ function build_shortest_proof( return proof } -export function get_missing_combinations(type: StructureType) { - const { implications, err: err_imp } = get_normalized_implications(type) - - if (err_imp) return { err: err_imp, missing_combinations: [] } - - const { rows: properties, err } = query<{ - id: string - dual_property_id: string | null - }>({ - sql: `SELECT id, dual_property_id FROM ${type}_properties ORDER BY lower(id)`, - }) - - if (err) return { err, missing_combinations: [] } - - const { rows: existing, err: err_existing } = query<{ - p: string - q: string - }>({ - sql: ` - SELECT DISTINCT a.property_id AS p, an.property_id AS q - FROM ${type}_property_assignments a - INNER JOIN ${type}_property_assignments an - ON a.${type}_id = an.${type}_id - WHERE a.is_satisfied = TRUE AND an.is_satisfied = FALSE - `, - }) - - if (err_existing) return { err: err_existing, missing_combinations: [] } - - const witnessed_pairs = new Set(existing.map(({ p, q }) => `${p}|${q}`)) - - const missing_combinations: [string, string][] = [] - - for (const p of properties) { - for (const q of properties) { - if (p.id === q.id) continue - - if (witnessed_pairs.has(`${p.id}|${q.id}`)) continue - - if ( - p.dual_property_id && - q.dual_property_id && - witnessed_pairs.has(`${p.dual_property_id}|${q.dual_property_id}`) - ) { - continue - } - - const contradiction = contradiction_worker( - new Set([p.id]), - new Set([q.id]), - implications, - ) - - if (!contradiction) missing_combinations.push([p.id, q.id]) - } - } - - return { missing_combinations, err: null } +function stringify_implication(implication: NormalizedImplication) { + return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` } diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts new file mode 100644 index 000000000..aa6a25830 --- /dev/null +++ b/src/lib/server/fetchers/category.ts @@ -0,0 +1,69 @@ +import type { + CategorySpecificDisplay, + SpecialMorphism, + SpecialObject, + StructureShort, +} from '$lib/commons/types' +import sql from 'sql-template-tag' +import { batch, query } from '$lib/server/db.catdat' +import { error } from '@sveltejs/kit' + +export function fetch_category(id: string) { + const { results, err } = batch< + [CategorySpecificDisplay, SpecialObject, SpecialMorphism] + >([ + // specific information for the category + sql` + SELECT c.objects, c.morphisms + FROM categories c + WHERE c.id = ${id} + `, + // special objects + sql` + SELECT s.type, s.description + FROM special_objects s + INNER JOIN special_object_types t ON t.type = s.type + WHERE s.category_id = ${id} + ORDER BY t.id + `, + // special morphisms + sql` + SELECT t.type, s.description, s.proof + FROM special_morphism_types t + LEFT JOIN special_morphisms s + ON s.type = t.type AND s.category_id = ${id} + ORDER BY t.id + `, + ]) + + if (err) error(500, 'Could not load category') + + const [categories, special_objects, special_morphisms] = results + + if (!categories.length) error(404, `Could not find category with ID '${id}'`) + + return { + ...categories[0], + special_objects, + special_morphisms, + } +} + +export function fetch_categories_with_missing_morphisms() { + const { rows, err } = query( + sql` + SELECT s.id, s.name, COUNT(*) AS count + FROM structures s + JOIN special_morphism_types t + LEFT JOIN special_morphisms m + ON m.category_id = s.id AND m.type = t.type + WHERE s.type = 'category' AND m.type IS NULL + GROUP BY s.id + ORDER BY lower(s.name); + `, + ) + + if (err) error(500, 'Failed to load data') + + return rows +} diff --git a/src/lib/server/compare.ts b/src/lib/server/fetchers/comparison.ts similarity index 71% rename from src/lib/server/compare.ts rename to src/lib/server/fetchers/comparison.ts index 9309ab387..23b56cb02 100644 --- a/src/lib/server/compare.ts +++ b/src/lib/server/fetchers/comparison.ts @@ -1,18 +1,16 @@ -import { error, type RequestEvent } from '@sveltejs/kit' +import { error } from '@sveltejs/kit' import { query } from '$lib/server/db.catdat' import { render_nested_formulas } from '$lib/server/formulas' import { MAX_STRUCTURES_COMPARE } from '$lib/commons/compare.utils' import type { ComparisonResult, StructureType } from '$lib/commons/types' import { PLURALS } from '$lib/commons/structures' +import { to_placeholders } from '$lib/server/utils' -export function compare_handler( - event: RequestEvent, +export function fetch_comparison_result( + compared_ids: string[], type: StructureType, + callback: () => void, ): ComparisonResult { - if (!event.params.ids) error(400, `No ${type} selected for comparison`) - - const compared_ids = event.params.ids?.split('/') - if (!compared_ids.length) error(400, `No ${type} selected for comparison`) if (compared_ids.length > MAX_STRUCTURES_COMPARE) { @@ -22,8 +20,6 @@ export function compare_handler( ) } - const placeholders = compared_ids.map(() => '?').join(', ') - const { rows, err: err_cat } = query<{ id: string name: string @@ -31,9 +27,10 @@ export function compare_handler( }>({ sql: ` SELECT id, name, notation - FROM ${PLURALS[type]} - WHERE id in (${placeholders})`, - values: compared_ids, + FROM structures + WHERE type = ? + AND id in (${to_placeholders(compared_ids)})`, + values: [type, ...compared_ids], }) if (err_cat) error(500, `Could not load ${PLURALS[type]}`) @@ -61,36 +58,35 @@ export function compare_handler( compared_ids.forEach((id, i) => { join_fragments.push(` - LEFT JOIN ${type}_property_assignments a${i} - ON a${i}.property_id = p.id AND a${i}.${type}_id = ? + LEFT JOIN property_assignments a${i} + ON a${i}.property_id = p.id AND a${i}.structure_id = ? `) values.push(id) }) - const stmt = ` + values.push(type) + + const comparison_query = ` SELECT p.id AS property_id, ${select_columns} - FROM ${type}_properties p + FROM properties p ${join_fragments.join('\n')} + WHERE p.type = ? ORDER BY lower(p.id)` const { rows: comparison_objects, err } = query>({ - sql: stmt, + sql: comparison_query, values, }) - if (err) error(500, 'Could not load properties') + if (err) error(500, 'Could not load comparison table') const comparison_table = comparison_objects.map((obj) => Object.values(obj)) - event.setHeaders({ - // shared cache for 30min - 'cache-control': 'public, max-age=0, s-maxage=1800', - }) + callback() return { - type, structures: render_nested_formulas(structures), comparison_table, } diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts new file mode 100644 index 000000000..d0785e099 --- /dev/null +++ b/src/lib/server/fetchers/content.ts @@ -0,0 +1,38 @@ +import type { PropertyShort, StructureShort } from '$lib/commons/types' +import { batch } from '$lib/server/db.catdat' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' + +export function fetch_category_references(content_id: string) { + const { results, err: err_categories } = batch< + [StructureShort, PropertyShort, { id: string }] + >([ + sql` + SELECT DISTINCT s.id, s.name + FROM property_assignments pa + INNER JOIN structures s ON s.id = pa.structure_id + WHERE + pa.type = 'category' + AND pa.proof LIKE '%/content/' || ${content_id} || '%' + + `, + sql` + SELECT id, relation FROM properties + WHERE + type = 'category' + AND description LIKE '%/content/' || ${content_id} || '%' + `, + sql` + SELECT id FROM implications + WHERE + type = 'category' + AND proof LIKE '%/content/' || ${content_id} || '%' + `, + ]) + + if (err_categories) error(500, 'Could not load context') + + const [categories, category_properties, category_implications] = results + + return { categories, category_properties, category_implications } +} diff --git a/src/lib/server/fetchers/functor.ts b/src/lib/server/fetchers/functor.ts new file mode 100644 index 000000000..c3a4adeaf --- /dev/null +++ b/src/lib/server/fetchers/functor.ts @@ -0,0 +1,38 @@ +import type { FunctorSpecificDisplay } from '$lib/commons/types' +import sql from 'sql-template-tag' +import { query } from '$lib/server/db.catdat' +import { error } from '@sveltejs/kit' + +export function fetch_functor(id: string) { + const { rows: functors, err } = query( + // specific information for the functor + sql` + SELECT + f.source, + f.target, + source.name AS source_name, + source.notation AS source_notation, + target.name AS target_name, + target.notation AS target_notation, + la.id AS left_adjoint, + la.name AS left_adjoint_name, + la.notation AS left_adjoint_notation, + ra.id AS right_adjoint, + ra.name AS right_adjoint_name, + ra.notation AS right_adjoint_notation + FROM functors f + INNER JOIN structures AS source ON source.id = f.source + INNER JOIN structures AS target ON target.id = f.target + LEFT JOIN structures AS la ON la.id = f.left_adjoint + LEFT JOIN functors AS rf ON rf.left_adjoint = f.id + LEFT JOIN structures AS ra ON ra.id = rf.id + WHERE f.id = ${id} + `, + ) + + if (err) error(500, 'Could not load functor') + + if (!functors.length) error(404, `Could not find functor with ID '${id}'`) + + return functors[0] +} diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts new file mode 100644 index 000000000..f96267c72 --- /dev/null +++ b/src/lib/server/fetchers/implication.ts @@ -0,0 +1,61 @@ +import { batch } from '$lib/server/db.catdat' +import sql from 'sql-template-tag' +import { error } from '@sveltejs/kit' +import type { + ImplicationDB, + MappedTypes, + StructureShort, + StructureType, +} from '$lib/commons/types' +import { display_implication } from '$lib/server/transforms' + +export function fetch_implication(type: StructureType, id: string) { + const { results, err } = batch< + [ImplicationDB, StructureShort, { map: string; mapped_type: StructureType }] + >([ + sql` + SELECT + id, + is_equivalence, + is_deduced, + dualized_from, + proof, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE id = ${id} + `, + sql` + SELECT DISTINCT s.id, s.name + FROM property_assignments pa + INNER JOIN structures s ON s.id = pa.structure_id + WHERE + pa.type = ${type} + AND pa.proof LIKE '%/' || ${type} || '-implication/' || ${id} || '%' + `, + sql` + SELECT map, mapped_type + FROM structure_maps + WHERE type = ${type} + `, + ]) + + if (err) error(500, 'Could not load implication') + + const [implications, structures, structure_maps] = results + + if (!implications.length) { + error(404, `Could not find implication with ID '${id}'`) + } + + const implication = display_implication(implications[0]) + + const mapped_types: MappedTypes = {} + + for (const { map, mapped_type } of structure_maps) { + mapped_types[map] = mapped_type + } + + return { implication, structures, mapped_types } +} diff --git a/src/lib/server/fetchers/implications.ts b/src/lib/server/fetchers/implications.ts new file mode 100644 index 000000000..594cbd0fb --- /dev/null +++ b/src/lib/server/fetchers/implications.ts @@ -0,0 +1,90 @@ +import { query } from '$lib/server/db.catdat' +import sql from 'sql-template-tag' +import { error } from '@sveltejs/kit' +import type { + ImplicationDB, + NormalizedImplication, + StructureType, +} from '$lib/commons/types' +import { display_implication } from '$lib/server/transforms' +import { parse_json_set, parse_nested_json_list } from '$lib/server/utils' + +export function fetch_implications(type: StructureType) { + const { rows, err } = query(sql` + SELECT + id, + is_equivalence, + is_deduced, + dualized_from, + proof, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE type = ${type} + ORDER BY lower(assumptions) || ' ' || lower(conclusions) + `) + + if (err) error(500, 'Could not load implications') + + const implications = rows.map(display_implication) + + return { implications } +} + +/** + * List of normalized implications of a given type that have no mapped assumptions + * (e.g. no source and no target assumptions in the case of functors), + * i.e. those that are universally true. Only those are relevant + * for the consistency check. + */ +export function get_normalized_implications(type: StructureType) { + // TODO: remove duplication with deduction script + + const { rows, err } = query<{ + id: string + is_equivalence: 0 | 1 + assumptions: string + mapped_assumptions: string + conclusions: string + }>( + sql` + SELECT + id, + is_equivalence, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE type = ${type} + `, + ) + + if (err) return { implications: null, err } + + const implications: NormalizedImplication[] = [] + + for (const impl of rows) { + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) + const mapped_assumptions = parse_nested_json_list(impl.mapped_assumptions) + + if (Object.values(mapped_assumptions).some((list) => list?.length)) continue + + for (const conclusion of conclusions) { + implications.push({ id: impl.id, assumptions, conclusion }) + } + + if (impl.is_equivalence) { + for (const assumption of assumptions) { + implications.push({ + id: impl.id, + assumptions: conclusions, + conclusion: assumption, + }) + } + } + } + + return { implications, err: null } +} diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts new file mode 100644 index 000000000..80996ed3e --- /dev/null +++ b/src/lib/server/fetchers/missing_data.ts @@ -0,0 +1,132 @@ +import { batch } from '$lib/server/db.catdat' +import sql from 'sql-template-tag' +import type { StructureShort, StructureType } from '$lib/commons/types' +import { error } from '@sveltejs/kit' +import { contradiction_worker } from '$lib/server/consistency' +import { get_normalized_implications } from './implications' + +export function fetch_missing_data(type: StructureType) { + const { results, err } = batch< + [ + StructureShort & { count: number }, + { id1: string; name1: string; id2: string; name2: string }, + { id: string; dual_property_id: string | null }, + { p: string; q: string }, + ] + >([ + // structures with unknown properties + sql` + SELECT s.id, s.name, COUNT(*) AS count + FROM structures s + INNER JOIN properties p + LEFT JOIN property_assignments pa + ON pa.structure_id = s.id + AND pa.property_id = p.id + WHERE + p.type = ${type} + AND s.type = ${type} + AND pa.property_id IS NULL + GROUP BY s.id + ORDER BY lower(s.name); + `, + // undistinguishable structure pairs + sql` + SELECT + s1.id AS id1, s1.name AS name1, + s2.id AS id2, s2.name AS name2 + FROM structures s1 + JOIN structures s2 + ON s1.id < s2.id + JOIN properties p + LEFT JOIN property_assignments a1 + ON a1.structure_id = s1.id AND a1.property_id = p.id + LEFT JOIN property_assignments a2 + ON a2.structure_id = s2.id AND a2.property_id = p.id + WHERE + p.type = ${type} + AND s1.type = ${type} + AND s2.type = ${type} + GROUP BY s1.id, s1.name, s2.id, s2.name + HAVING SUM( + CASE + WHEN a1.is_satisfied IS a2.is_satisfied THEN 0 + ELSE 1 + END + ) = 0; + `, + // properties + sql` + SELECT id, dual_property_id + FROM properties + WHERE type = ${type} + ORDER BY lower(id) + `, + // witnessed property combinations of the form "p and not q" + sql` + SELECT DISTINCT + a.property_id AS p, + an.property_id AS q + FROM property_assignments a + INNER JOIN property_assignments an + ON a.structure_id = an.structure_id + WHERE + a.type = ${type} + AND an.type = ${type} + AND a.is_satisfied = TRUE + AND an.is_satisfied = FALSE + `, + ]) + + if (err) error(500, 'Failed to load data') + + const [ + structures_with_unknown_properties, + undistinguishable_structure_pairs, + properties, + witnessed_pairs, + ] = results + + const total_unknown_property_pairs = structures_with_unknown_properties.reduce( + (total, item) => item.count + total, + 0, + ) + + const { implications, err: err_imp } = get_normalized_implications(type) + + if (err_imp) error(500, 'Failed to load data') + + const witnessed_pairs_set = new Set(witnessed_pairs.map(({ p, q }) => `${p}|${q}`)) + + const missing_combinations: [string, string][] = [] + + for (const p of properties) { + for (const q of properties) { + if (p.id === q.id) continue + + if (witnessed_pairs_set.has(`${p.id}|${q.id}`)) continue + + if ( + p.dual_property_id && + q.dual_property_id && + witnessed_pairs_set.has(`${p.dual_property_id}|${q.dual_property_id}`) + ) { + continue + } + + const contradiction = contradiction_worker( + new Set([p.id]), + new Set([q.id]), + implications, + ) + + if (!contradiction) missing_combinations.push([p.id, q.id]) + } + } + + return { + structures_with_unknown_properties, + undistinguishable_structure_pairs, + total_unknown_property_pairs, + missing_combinations, + } +} diff --git a/src/lib/server/fetchers/properties.ts b/src/lib/server/fetchers/properties.ts new file mode 100644 index 000000000..89d270fce --- /dev/null +++ b/src/lib/server/fetchers/properties.ts @@ -0,0 +1,58 @@ +import type { GroupedPropertyShort, StructureType } from '$lib/commons/types' +import sql from 'sql-template-tag' +import { query } from '$lib/server/db.catdat' +import { error } from '@sveltejs/kit' + +export function get_property_ids(type: StructureType) { + const { rows, err } = query<{ id: string }>( + sql` + SELECT id FROM properties + WHERE type = ${type} + ORDER BY lower(id) + `, + ) + + if (err) error(500, 'Failed to load properties') + + return rows.map(({ id }) => id) +} + +export function get_grouped_properties(type: StructureType) { + const { rows: properties, err } = query(sql` + SELECT id, relation, dual_property_id + FROM properties + WHERE type = ${type} + ORDER BY lower(id) + `) + + if (err) error(500, 'Failed to load properties') + + const seen = new Set() + + const grouped_properties: typeof properties = [] + + for (const p of properties) { + if (seen.has(p.id) || (p.dual_property_id && seen.has(p.dual_property_id))) { + continue + } + + if (p.id.startsWith('co') && p.dual_property_id) { + const swap = { + id: p.dual_property_id, + dual_property_id: p.id, + relation: p.relation, + } + grouped_properties.push(swap) + } else { + grouped_properties.push(p) + } + + seen.add(p.id) + if (p.dual_property_id) seen.add(p.dual_property_id) + } + + const total = properties.length + const grouped_total = grouped_properties.length + + return { grouped_properties, total, grouped_total } +} diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts new file mode 100644 index 000000000..39ab64bc3 --- /dev/null +++ b/src/lib/server/fetchers/property.ts @@ -0,0 +1,132 @@ +import type { + ImplicationDB, + StructureShort, + PropertyDB, + StructureType, +} from '$lib/commons/types' +import { batch } from '$lib/server/db.catdat' +import { display_implication, display_property } from '$lib/server/transforms' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' + +export function fetch_property(type: StructureType, id: string) { + const { results, err } = batch< + [ + PropertyDB, + { id: string }, + ImplicationDB, + StructureShort & { is_satisfied: 0 | 1 | null }, + StructureShort, + ] + >([ + // basic information + sql` + SELECT + id, + relation, + description, + dual_property_id, + nlab_link, + invariant_under_equivalences + FROM properties + WHERE id = ${id} + `, + // related properties + sql` + SELECT related_property_id AS id + FROM related_properties + WHERE property_id = ${id} + ORDER BY lower(id) + `, + // relevant implications + sql` + SELECT + id, + is_equivalence, + is_deduced, + dualized_from, + proof, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE type = ${type} + AND ( + EXISTS ( + SELECT 1 + FROM json_each(conclusions) + WHERE value = ${id} + ) + OR + EXISTS ( + SELECT 1 + FROM json_each(assumptions) + WHERE value = ${id} + ) + ) + ORDER BY lower(assumptions) || ' ' || lower(conclusions) + `, + // known structures + sql` + SELECT s.id, s.name, pa.is_satisfied + FROM property_assignments pa + INNER JOIN structures s ON s.id = pa.structure_id + WHERE + s.type = ${type} + AND pa.property_id = ${id} + ORDER BY lower(s.name) + `, + // unknown structures + sql` + SELECT s.id, s.name + FROM structures s + LEFT JOIN property_assignments pa + ON pa.structure_id = s.id + AND pa.property_id = ${id} + WHERE + s.type = ${type} + AND pa.property_id IS NULL + ORDER BY lower(s.name) + `, + ]) + + if (err) error(500, 'Could not load property') + + const [ + properties, + related, + relevant_implications_db, + known_structures, + unknown_structures, + ] = results + + if (!properties.length) { + error(404, `Could not find property with ID '${id}'`) + } + + const property = display_property(properties[0]) + + const related_properties = related.map(({ id }) => id) + + const examples = known_structures.filter((f) => f.is_satisfied === 1) + const counterexamples = known_structures.filter((f) => f.is_satisfied === 0) + const undecidable_structures = known_structures.filter((f) => f.is_satisfied === null) + + const relevant_implications = relevant_implications_db.map(display_implication) + + for (const impl of relevant_implications) { + if (!impl.is_equivalence && impl.conclusions.includes(id)) { + impl.conclusions = [id] + } + } + + return { + property, + related_properties, + examples, + counterexamples, + unknown_structures, + undecidable_structures, + relevant_implications, + } +} diff --git a/src/lib/server/search.ts b/src/lib/server/fetchers/search.ts similarity index 79% rename from src/lib/server/search.ts rename to src/lib/server/fetchers/search.ts index cdade48e3..c363df587 100644 --- a/src/lib/server/search.ts +++ b/src/lib/server/fetchers/search.ts @@ -1,23 +1,18 @@ -import type { RequestEvent } from '@sveltejs/kit' import { decode_property_ID } from '$lib/commons/property.url' import { query } from '$lib/server/db.catdat' import { error } from '@sveltejs/kit' import { SEARCH_SEPARATOR } from '$lib/commons/search.config' import { get_contradiction } from '$lib/server/consistency' import type { SearchResults, StructureShort, StructureType } from '$lib/commons/types' -import { to_placeholders } from './utils' -import { PLURALS } from '$lib/commons/structures' - -function cache_page(event: RequestEvent) { - event.setHeaders({ - 'cache-control': 'public, max-age=0, s-maxage=1800', // shared cache for 30min - }) -} - -export function search_handler(event: RequestEvent, type: StructureType): SearchResults { - const satisfied_query = event.url.searchParams.get('satisfied') - const unsatisfied_query = event.url.searchParams.get('unsatisfied') - +import { to_placeholders } from '$lib/server/utils' +import sql from 'sql-template-tag' + +export function fetch_search_results( + satisfied_query: string | null, + unsatisfied_query: string | null, + type: StructureType, + callback: () => void, +): SearchResults { if (!satisfied_query && !unsatisfied_query) { error(400, 'No properties selected') } @@ -25,9 +20,11 @@ export function search_handler(event: RequestEvent, type: StructureType): Search const { rows: all_properties_objects, err: err_all } = query<{ id: string dual_property_id: string | null - }>({ - sql: `SELECT id, dual_property_id FROM ${type}_properties ORDER BY lower(id)`, - }) + }>(sql` + SELECT id, dual_property_id FROM properties + WHERE type = ${type} + ORDER BY lower(id) + `) if (err_all) error(500, 'Failed to load properties') @@ -83,10 +80,9 @@ export function search_handler(event: RequestEvent, type: StructureType): Search if (err_con) error(500, 'Consistency check failed') if (contradiction) { - cache_page(event) + callback() return { - type, contradiction, satisfied_properties, unsatisfied_properties, @@ -100,10 +96,12 @@ export function search_handler(event: RequestEvent, type: StructureType): Search const all_selected_properties = [...satisfied_properties, ...unsatisfied_properties] const search_query = ` - SELECT s.id, s.name FROM ${PLURALS[type]} s - INNER JOIN ${type}_property_assignments a ON a.${type}_id = s.id - WHERE property_id IN (${to_placeholders(all_selected_properties)}) - GROUP BY ${type}_id + SELECT s.id, s.name FROM structures s + INNER JOIN property_assignments a ON a.structure_id = s.id + WHERE + a.type = ? AND s.type = ? + AND property_id IN (${to_placeholders(all_selected_properties)}) + GROUP BY structure_id HAVING SUM ( CASE @@ -130,6 +128,8 @@ export function search_handler(event: RequestEvent, type: StructureType): Search const { rows: found_structures, err } = query({ sql: search_query, values: [ + type, + type, ...all_selected_properties, ...satisfied_properties, ...unsatisfied_properties, @@ -138,10 +138,9 @@ export function search_handler(event: RequestEvent, type: StructureType): Search if (err) error(500, 'Search failed') - cache_page(event) + callback() return { - type, contradiction: null, satisfied_properties, unsatisfied_properties, diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts new file mode 100644 index 000000000..05d564a1d --- /dev/null +++ b/src/lib/server/fetchers/structure.ts @@ -0,0 +1,155 @@ +import type { + CommentObject, + PropertyAssignmentDB, + PropertyShort, + RelatedStructure, + StructureDisplay, + StructureShort, + StructureType, + TagObject, +} from '$lib/commons/types' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' +import { batch } from '$lib/server/db.catdat' +import { display_property_assignment } from '$lib/server/transforms' + +export function fetch_structure(type: StructureType, id: string) { + const { err, results } = batch< + [ + StructureDisplay, + RelatedStructure, + TagObject, + PropertyAssignmentDB, + PropertyShort, + StructureShort, + CommentObject, + ] + >([ + // basic information + sql` + SELECT + s.id, + s.name, + s.notation, + s.description, + s.nlab_link, + s.dual_structure_id, + ds.name AS dual_structure_name, + ds.notation AS dual_structure_notation + FROM structures s + LEFT JOIN structures ds ON ds.id = s.dual_structure_id + WHERE s.id = ${id} + `, + // related structures + sql` + SELECT + c.id, + c.name, + c.notation + FROM related_structures r + INNER JOIN structures c ON c.id = r.related_structure_id + WHERE r.structure_id = ${id} + ORDER BY lower(c.name) + `, + // tags + sql` + SELECT st.tag + FROM structure_tag_assignments st + INNER JOIN tags t ON t.tag = st.tag + WHERE t.type = ${type} AND st.structure_id = ${id} + ORDER BY t.id + `, + // properties + sql` + SELECT + pa.property_id AS id, + pa.is_satisfied, + pa.proof, + pa.is_deduced, + p.relation + FROM property_assignments pa + INNER JOIN properties p ON p.id = pa.property_id + WHERE pa.structure_id = ${id} + ORDER BY pa.id + `, + // unknown properties + sql` + SELECT p.id, p.relation + FROM properties p + WHERE type = ${type} AND NOT EXISTS ( + SELECT 1 FROM property_assignments + WHERE structure_id = ${id} AND property_id = p.id + ) + ORDER BY lower(p.id) + `, + // undistinguishable structures + sql` + SELECT u.id, u.name + FROM structures u + JOIN properties p + LEFT JOIN property_assignments pa + ON pa.structure_id = ${id} + AND pa.property_id = p.id + LEFT JOIN property_assignments up + ON up.structure_id = u.id + AND up.property_id = p.id + WHERE + p.type = ${type} + AND u.type = ${type} + AND u.id != ${id} + GROUP BY u.id, u.name + HAVING SUM( + CASE + WHEN pa.is_satisfied IS up.is_satisfied THEN 0 + ELSE 1 + END + ) = 0; + `, + // comments + sql` + SELECT id, comment FROM structure_comments + WHERE structure_id = ${id} + `, + ]) + + if (err) error(500, `Could not load ${type} with ID ${id}`) + + const [ + structures, + related_structures, + tag_objects, + properties_db, + unknown_properties, + undistinguishable_structures, + comments, + ] = results + + if (!structures.length) error(404, `Could not find ${type} with ID '${id}'`) + + const structure = structures[0] + const tags = tag_objects.map(({ tag }) => tag) + + const satisfied_properties = properties_db + .filter((obj) => obj.is_satisfied === 1) + .map(display_property_assignment) + + const unsatisfied_properties = properties_db + .filter((obj) => obj.is_satisfied === 0) + .map(display_property_assignment) + + const undecidable_properties = properties_db + .filter((obj) => obj.is_satisfied === null) + .map(display_property_assignment) + + return { + structure, + related_structures, + tags, + satisfied_properties, + unsatisfied_properties, + unknown_properties, + undecidable_properties, + undistinguishable_structures, + comments, + } +} diff --git a/src/lib/server/fetchers/structures.ts b/src/lib/server/fetchers/structures.ts new file mode 100644 index 000000000..d61ee10e8 --- /dev/null +++ b/src/lib/server/fetchers/structures.ts @@ -0,0 +1,58 @@ +import { capitalize } from '$lib/client/utils' +import { PLURALS } from '$lib/commons/structures' +import type { StructureShort, StructureType, TagObject } from '$lib/commons/types' +import { batch, query } from '$lib/server/db.catdat' +import { error } from '@sveltejs/kit' +import sql from 'sql-template-tag' + +export function fetch_structures(type: StructureType) { + const { rows: structures, err } = query(sql` + SELECT id, name + FROM structures + WHERE type = ${type} + ORDER BY lower(name) + `) + + if (err) error(500, `${capitalize(PLURALS[type])} could not be loaded`) + + return { structures } +} + +export function fetch_structures_and_tags(type: StructureType) { + const { results, err } = batch<[StructureShort, TagObject]>([ + sql` + SELECT id, name + FROM structures + WHERE type = ${type} + ORDER BY lower(name)`, + sql` + SELECT tag + FROM tags + WHERE type = ${type} + ORDER BY id + `, + ]) + + if (err) error(500, `${capitalize(PLURALS[type])} could not be loaded`) + + const [structures, tag_objects] = results + + const tags = tag_objects.map(({ tag }) => tag) + + return { structures, tags } +} + +export function fetch_tagged_structures(type: StructureType, tag: string) { + const { rows: structures, err } = query(sql` + SELECT s.id, s.name + FROM structure_tag_assignments t + INNER JOIN structures s + ON s.id = t.structure_id + WHERE t.tag = ${tag} AND t.type = ${type} + ORDER BY lower(name) + `) + + if (err) error(500, `${capitalize(PLURALS[type])} could not be loaded`) + + return { structures, tag } +} diff --git a/src/lib/server/fetchers/tags.ts b/src/lib/server/fetchers/tags.ts new file mode 100644 index 000000000..6a925b399 --- /dev/null +++ b/src/lib/server/fetchers/tags.ts @@ -0,0 +1,13 @@ +import type { StructureType, TagObject } from '$lib/commons/types' +import sql from 'sql-template-tag' +import { query } from '$lib/server/db.catdat' + +export function fetch_tags(type: StructureType) { + const { rows, err } = query(sql` + SELECT tag FROM tags WHERE type = ${type} + `) + + if (err) throw new Error('Database error: Failed to load tags') + + return rows +} diff --git a/src/lib/server/implications.ts b/src/lib/server/implications.ts deleted file mode 100644 index 2160e1272..000000000 --- a/src/lib/server/implications.ts +++ /dev/null @@ -1,114 +0,0 @@ -import sql from 'sql-template-tag' -import { query } from './db.catdat' -import { parse_json_set } from './utils' -import type { StructureType } from '$lib/commons/types' - -// TODO: If possible, remove the code duplication with deduction and redundancy scripts. - -export type NormalizedImplication = { - id: string - assumptions: Set - conclusion: string -} - -/** - * List of normalized implications of a given type of structure. - */ -export function get_normalized_implications(type: StructureType) { - if (type === 'category') return get_normalized_category_implications() - if (type === 'functor') return get_normalized_functor_implications() - throw new Error('Unsupported type') -} - -/** - * List of normalized implications of categories. - */ -function get_normalized_category_implications() { - const { rows, err } = query<{ - id: string - assumptions: string - conclusions: string - is_equivalence: 0 | 1 - }>( - sql`SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`, - ) - - if (err) return { implications: null, err } - - const implications: NormalizedImplication[] = [] - - for (const impl of rows) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - - for (const conclusion of conclusions) { - implications.push({ id: impl.id, assumptions, conclusion }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption, - }) - } - } - } - - return { implications, err: null } -} - -/** - * List of normalized implications of functors that have no source or target - * assumptions, i.e. those that are universally true. Only those are relevant - * for the consistency check. - */ -function get_normalized_functor_implications() { - const { rows, err } = query<{ - id: string - assumptions: string - conclusions: string - source_assumptions: string - target_assumptions: string - is_equivalence: 0 | 1 - }>( - sql` - SELECT id, assumptions, source_assumptions, target_assumptions, - conclusions, is_equivalence - FROM functor_implications_view`, - ) - - if (err) return { implications: null, err } - - const implications: NormalizedImplication[] = [] - - for (const impl of rows) { - const assumptions = parse_json_set(impl.assumptions) - const source_assumptions = parse_json_set(impl.source_assumptions) - const target_assumptions = parse_json_set(impl.target_assumptions) - const conclusions = parse_json_set(impl.conclusions) - - if (source_assumptions.size > 0 || target_assumptions.size > 0) continue - - for (const conclusion of conclusions) { - implications.push({ id: impl.id, assumptions, conclusion }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption, - }) - } - } - } - - return { implications, err: null } -} - -export function stringify_implication(implication: NormalizedImplication) { - return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` -} diff --git a/src/lib/server/properties.ts b/src/lib/server/properties.ts deleted file mode 100644 index bfe464596..000000000 --- a/src/lib/server/properties.ts +++ /dev/null @@ -1,13 +0,0 @@ -import type { StructureType } from '$lib/commons/types' -import { query } from './db.catdat' -import { error } from '@sveltejs/kit' - -export function get_property_ids(type: StructureType) { - const { rows, err } = query<{ id: string }>({ - sql: `SELECT id FROM ${type}_properties ORDER BY lower(id)`, - }) - - if (err) error(500, 'Failed to load properties') - - return rows.map(({ id }) => id) -} diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index 90fa3e7be..fa5685bac 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -6,6 +6,7 @@ import type { ImplicationDB, ImplicationDisplay, } from '$lib/commons/types' +import { parse_nested_json_list } from './utils' export function display_property(property: PropertyDB): PropertyDisplay { return { @@ -69,12 +70,7 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp dualized_from: implication.dualized_from, proof: implication.proof, assumptions: JSON.parse(implication.assumptions), - source_assumptions: implication.source_assumptions - ? JSON.parse(implication.source_assumptions) - : undefined, - target_assumptions: implication.target_assumptions - ? JSON.parse(implication.target_assumptions) - : undefined, conclusions: JSON.parse(implication.conclusions), + mapped_assumptions: parse_nested_json_list(implication.mapped_assumptions), } } diff --git a/src/lib/server/utils.ts b/src/lib/server/utils.ts index ab5fbc3c5..09a9a3f75 100644 --- a/src/lib/server/utils.ts +++ b/src/lib/server/utils.ts @@ -1,3 +1,5 @@ +import type { RequestEvent } from '@sveltejs/kit' + export function is_object(obj: unknown): obj is Record { return obj != null && obj.constructor.name === 'Object' } @@ -18,3 +20,17 @@ export const sleep = (delay: number) => new Promise((res) => setTimeout(re export function parse_json_set(json: string): Set { return new Set(JSON.parse(json)) } + +export function parse_nested_json_list(json: string): Partial> { + const obj = JSON.parse(json) + const result: Partial> = {} + for (const key in obj) { + result[key] = JSON.parse(obj[key]) + } + return result +} + +export function cache_page(event: RequestEvent) { + // shared cache for 30min + event.setHeaders({ 'cache-control': 'public, max-age=0, s-maxage=1800' }) +} diff --git a/src/pages/ComparisonResultPage.svelte b/src/pages/ComparisonResultPage.svelte index 3db0ddc7f..c7aaa5ba3 100644 --- a/src/pages/ComparisonResultPage.svelte +++ b/src/pages/ComparisonResultPage.svelte @@ -2,7 +2,7 @@ import MetaData from '$components/MetaData.svelte' import { get_property_url } from '$lib/commons/property.url' import { PLURALS } from '$lib/commons/structures' - import type { ComparisonResult } from '$lib/commons/types' + import type { ComparisonResult, StructureType } from '$lib/commons/types' import { faCheck, faQuestion, @@ -11,7 +11,9 @@ } from '@fortawesome/free-solid-svg-icons' import Fa from 'svelte-fa' - let { type, structures, comparison_table }: ComparisonResult = $props() + type Props = { type: StructureType } & ComparisonResult + + let { type, structures, comparison_table }: Props = $props() const icon_config: Record = { yes: faCheck, diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index f2647d937..39db6aa7d 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -8,19 +8,20 @@ import Fa from 'svelte-fa' import type { ImplicationDisplay, + MappedTypes, StructureShort, StructureType, } from '$lib/commons/types' import { PLURALS } from '$lib/commons/structures' type Props = { + type: StructureType implication: ImplicationDisplay structures: StructureShort[] - type: StructureType - associated_type?: StructureType + mapped_types: MappedTypes } - let { implication, structures, type, associated_type = type }: Props = $props() + let { type, implication, structures, mapped_types }: Props = $props() @@ -38,31 +39,20 @@ {/each}

    -{#if implication.source_assumptions?.length} -

    - Assumptions on source {associated_type}: - - {#each implication.source_assumptions as property, index} - {property}{#if index < implication.source_assumptions.length - 1} - ,  - {/if} - {/each} -

    -{/if} - -{#if implication.target_assumptions?.length} -

    - Assumptions on target {associated_type}: - - {#each implication.target_assumptions as property, index} - {property}{#if index < implication.target_assumptions.length - 1} - ,  - {/if} - {/each} -

    -{/if} +{#each Object.entries(implication.mapped_assumptions) as [map, list]} + {#if list?.length} +

    + Assumptions on {map} {mapped_types[map]}: + + {#each list as property, index} + {property}{#if index < list.length - 1} + ,  + {/if} + {/each} +

    + {/if} +{/each}

    Conclusions: diff --git a/src/pages/SearchResultsPage.svelte b/src/pages/SearchResultsPage.svelte index 136a70f80..ed21878e2 100644 --- a/src/pages/SearchResultsPage.svelte +++ b/src/pages/SearchResultsPage.svelte @@ -7,9 +7,11 @@ import { pluralize } from '$lib/client/utils' import Fa from 'svelte-fa' import { faWarning } from '@fortawesome/free-solid-svg-icons' - import type { SearchResults } from '$lib/commons/types' + import type { SearchResults, StructureType } from '$lib/commons/types' import { PLURALS } from '$lib/commons/structures' + type Props = { type: StructureType } & SearchResults + let { type, satisfied_properties, @@ -19,7 +21,7 @@ dual_search_available, found_structures, contradiction, - }: SearchResults = $props() + }: Props = $props() function get_dual_search_results_link() { if (!dual_search_available || !browser) return '/' diff --git a/src/routes/+layout.svelte b/src/routes/+layout.svelte index c2fc92a35..f6c694cb3 100644 --- a/src/routes/+layout.svelte +++ b/src/routes/+layout.svelte @@ -7,6 +7,7 @@ import NavMobile from '$components/NavMobile.svelte' import Popup from '$components/Popup.svelte' import { track_visit } from '$lib/client/track' + import { get_selected_type } from '$lib/commons/structures' import type { StructureType } from '$lib/commons/types' import { tracking } from '$lib/states/tracking.svelte' import './app.css' @@ -31,20 +32,7 @@ let nav_dialog = $state(null) - let selected_type = $state( - page.url.pathname.startsWith('/functor') ? 'functor' : 'category', - ) - - $effect(() => { - if (page.url.pathname.startsWith('/functor')) { - selected_type = 'functor' - } else if ( - page.url.pathname.startsWith('/category') || - page.url.pathname.startsWith('/categories') - ) { - selected_type = 'category' - } - }) + let selected_type = $derived(get_selected_type(page.url.pathname)) diff --git a/src/routes/admin/+page.server.ts b/src/routes/admin/+page.server.ts index cfc35666f..dde82f9a9 100644 --- a/src/routes/admin/+page.server.ts +++ b/src/routes/admin/+page.server.ts @@ -3,6 +3,6 @@ import { has_session } from './sessions' export const prerender = false -export const load = async (event) => { +export const load = (event) => { if (!has_session(event)) redirect(307, '/admin/login') } diff --git a/src/routes/categories/+page.server.ts b/src/routes/categories/+page.server.ts index dedbc1761..cbedafab7 100644 --- a/src/routes/categories/+page.server.ts +++ b/src/routes/categories/+page.server.ts @@ -1,19 +1,5 @@ -import type { StructureShort, TagObject } from '$lib/commons/types' -import { batch } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' +import { fetch_structures_and_tags } from '$lib/server/fetchers/structures' -export const load = async () => { - const { results, err } = batch<[StructureShort, TagObject]>([ - sql`SELECT id, name FROM categories ORDER BY lower(name)`, - sql`SELECT tag FROM category_tags ORDER BY id`, - ]) - - if (err) error(500, 'Categories could not be loaded') - - const [categories, tag_objects] = results - - const tags = tag_objects.map(({ tag }) => tag) - - return { categories, tags } +export const load = () => { + return fetch_structures_and_tags('category') } diff --git a/src/routes/categories/+page.svelte b/src/routes/categories/+page.svelte index c743479f0..7a38c6f9f 100644 --- a/src/routes/categories/+page.svelte +++ b/src/routes/categories/+page.svelte @@ -4,4 +4,4 @@ let { data } = $props() - + diff --git a/src/routes/categories/[tag]/+page.server.ts b/src/routes/categories/[tag]/+page.server.ts index 610a8dcb9..7c1f5fc06 100644 --- a/src/routes/categories/[tag]/+page.server.ts +++ b/src/routes/categories/[tag]/+page.server.ts @@ -1,26 +1,11 @@ -import type { StructureShort, TagObject } from '$lib/commons/types' -import { query } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' import type { EntryGenerator } from './$types' +import { fetch_tagged_structures } from '$lib/server/fetchers/structures' +import { fetch_tags } from '$lib/server/fetchers/tags' -export const entries: EntryGenerator = async () => { - const { rows, err } = query(sql`SELECT tag FROM category_tags`) - if (err) throw new Error('Database error: Failed to load tags') - return rows +export const entries: EntryGenerator = () => { + return fetch_tags('category') } -export const load = async (event) => { - const tag = event.params.tag - - const { rows: categories, err } = query(sql` - SELECT c.id, c.name FROM categories c - LEFT JOIN category_tag_assignments t ON c.id = t.category_id - WHERE t.tag = ${tag} - ORDER BY lower(name) - `) - - if (err) error(500, 'Categories could not be loaded') - - return { categories, tag } +export const load = (event) => { + return fetch_tagged_structures('category', event.params.tag) } diff --git a/src/routes/categories/[tag]/+page.svelte b/src/routes/categories/[tag]/+page.svelte index 66a2626ed..e1fa0be6f 100644 --- a/src/routes/categories/[tag]/+page.svelte +++ b/src/routes/categories/[tag]/+page.svelte @@ -4,4 +4,4 @@ let { data } = $props() - + diff --git a/src/routes/category-comparison/+page.server.ts b/src/routes/category-comparison/+page.server.ts index 7ed719946..5095734eb 100644 --- a/src/routes/category-comparison/+page.server.ts +++ b/src/routes/category-comparison/+page.server.ts @@ -1,14 +1,5 @@ -import type { StructureShort } from '$lib/commons/types' -import sql from 'sql-template-tag' -import { query } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' +import { fetch_structures } from '$lib/server/fetchers/structures' -export const load = async () => { - const { rows: categories, err } = query(sql` - SELECT id, name FROM categories ORDER BY lower(name) - `) - - if (err) error(500, 'Categories could not be loaded') - - return { categories } +export const load = () => { + return fetch_structures('category') } diff --git a/src/routes/category-comparison/+page.svelte b/src/routes/category-comparison/+page.svelte index ec739ec11..e09ee6646 100644 --- a/src/routes/category-comparison/+page.svelte +++ b/src/routes/category-comparison/+page.svelte @@ -4,4 +4,4 @@ let { data } = $props() - + diff --git a/src/routes/category-comparison/[...ids]/+page.server.ts b/src/routes/category-comparison/[...ids]/+page.server.ts index 110bb791f..8b747a9c7 100644 --- a/src/routes/category-comparison/[...ids]/+page.server.ts +++ b/src/routes/category-comparison/[...ids]/+page.server.ts @@ -1,7 +1,12 @@ -import { compare_handler } from '$lib/server/compare' +import { fetch_comparison_result } from '$lib/server/fetchers/comparison' +import { cache_page } from '$lib/server/utils' export const prerender = false -export const load = async (event) => { - return compare_handler(event, 'category') +export const load = (event) => { + const compared_ids = event.params.ids.split('/') + + return fetch_comparison_result(compared_ids, 'category', () => { + cache_page(event) + }) } diff --git a/src/routes/category-comparison/[...ids]/+page.svelte b/src/routes/category-comparison/[...ids]/+page.svelte index bc78c0081..e1fd975e3 100644 --- a/src/routes/category-comparison/[...ids]/+page.svelte +++ b/src/routes/category-comparison/[...ids]/+page.svelte @@ -4,4 +4,4 @@ let { data } = $props() - + diff --git a/src/routes/category-implication/[id]/+page.server.ts b/src/routes/category-implication/[id]/+page.server.ts index 19babe02f..0483fd870 100644 --- a/src/routes/category-implication/[id]/+page.server.ts +++ b/src/routes/category-implication/[id]/+page.server.ts @@ -1,43 +1,8 @@ -import type { StructureShort, ImplicationDB } from '$lib/commons/types' -import { batch } from '$lib/server/db.catdat' +import { fetch_implication } from '$lib/server/fetchers/implication' import { render_nested_formulas } from '$lib/server/formulas' -import { display_implication } from '$lib/server/transforms' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' -export const load = async (event) => { +export const load = (event) => { const id = event.params.id - const { results, err } = batch<[ImplicationDB, StructureShort]>([ - sql` - SELECT - id, - is_equivalence, - is_deduced, - dualized_from, - proof, - assumptions, - conclusions - FROM category_implications_view - WHERE id = ${id} - `, - sql` - SELECT c.id, c.name FROM categories c - WHERE EXISTS ( - SELECT 1 FROM category_property_assignments cp - WHERE cp.category_id = c.id - AND cp.proof LIKE '%/category-implication/' || ${id} || '%' - ) - `, - ]) - - if (err) error(500, 'Could not load implication') - - const [implications, categories] = results - - if (!implications.length) error(404, `Could not find implication with ID '${id}'`) - - const implication = display_implication(implications[0]) - - return render_nested_formulas({ implication, categories }) + return render_nested_formulas(fetch_implication('category', id)) } diff --git a/src/routes/category-implication/[id]/+page.svelte b/src/routes/category-implication/[id]/+page.svelte index dd3da925f..af2c4f39c 100644 --- a/src/routes/category-implication/[id]/+page.svelte +++ b/src/routes/category-implication/[id]/+page.svelte @@ -1,10 +1,7 @@ - + diff --git a/src/routes/category-implications/+page.server.ts b/src/routes/category-implications/+page.server.ts index 385f34f81..2b5992bed 100644 --- a/src/routes/category-implications/+page.server.ts +++ b/src/routes/category-implications/+page.server.ts @@ -1,27 +1,8 @@ import { render_nested_formulas } from '$lib/server/formulas' -import { query } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' -import { error } from '@sveltejs/kit' -import type { ImplicationDB } from '$lib/commons/types' -import { display_implication } from '$lib/server/transforms' +import { fetch_implications } from '$lib/server/fetchers/implications' -export const load = async () => { - const { rows, err } = query(sql` - SELECT - id, - is_equivalence, - is_deduced, - dualized_from, - proof, - assumptions, - conclusions - FROM category_implications_view - ORDER BY lower(assumptions) || ' ' || lower(conclusions) - `) - - if (err) error(500, 'Could not load implications') - - const implications = rows.map(display_implication) +export const load = () => { + const { implications } = fetch_implications('category') return render_nested_formulas({ implications }) } diff --git a/src/routes/category-properties/+page.server.ts b/src/routes/category-properties/+page.server.ts index ead9518b7..39f9c2a92 100644 --- a/src/routes/category-properties/+page.server.ts +++ b/src/routes/category-properties/+page.server.ts @@ -1,42 +1,5 @@ -import type { GroupedPropertyShort } from '$lib/commons/types' -import { query } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' +import { get_grouped_properties } from '$lib/server/fetchers/properties' -export const load = async () => { - const { rows: properties, err } = query(sql` - SELECT id, relation, dual_property_id FROM category_properties - ORDER BY lower(id) - `) - - if (err) error(500, 'Could not load properties') - - const seen = new Set() - - const grouped_properties: typeof properties = [] - - for (const p of properties) { - if (seen.has(p.id) || (p.dual_property_id && seen.has(p.dual_property_id))) { - continue - } - - if (p.id.startsWith('co') && p.dual_property_id) { - const swap = { - id: p.dual_property_id, - dual_property_id: p.id, - relation: p.relation, - } - grouped_properties.push(swap) - } else { - grouped_properties.push(p) - } - - seen.add(p.id) - if (p.dual_property_id) seen.add(p.dual_property_id) - } - - const total = properties.length - const grouped_total = grouped_properties.length - - return { grouped_properties, total, grouped_total } +export const load = () => { + return get_grouped_properties('category') } diff --git a/src/routes/category-properties/+page.svelte b/src/routes/category-properties/+page.svelte index 6fb4b8cff..72c16cdd3 100644 --- a/src/routes/category-properties/+page.svelte +++ b/src/routes/category-properties/+page.svelte @@ -1,5 +1,6 @@ diff --git a/src/routes/category-property/[id]/+page.server.ts b/src/routes/category-property/[id]/+page.server.ts index 5938493fc..f6b3b19d2 100644 --- a/src/routes/category-property/[id]/+page.server.ts +++ b/src/routes/category-property/[id]/+page.server.ts @@ -1,124 +1,11 @@ -import { error } from '@sveltejs/kit' import { render_nested_formulas } from '$lib/server/formulas' import { decode_property_ID } from '$lib/commons/property.url' -import { batch } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' -import type { StructureShort, PropertyDB } from '$lib/commons/types' -import type { ImplicationDB } from '$lib/commons/types' -import { display_implication, display_property } from '$lib/server/transforms' +import { fetch_property } from '$lib/server/fetchers/property' -export const load = async (event) => { +export const load = (event) => { const id = decode_property_ID(event.params.id) - const { results, err } = batch< - [ - PropertyDB, - { id: string }, - ImplicationDB, - StructureShort & { is_satisfied: 0 | 1 | null }, - StructureShort, - ] - >([ - // basic information - sql` - SELECT - id, - relation, - description, - dual_property_id, - nlab_link, - invariant_under_equivalences - FROM category_properties - WHERE id = ${id} - `, - // related properties - sql` - SELECT related_property_id AS id - FROM related_category_properties - WHERE property_id = ${id} - ORDER BY lower(id) - `, - // relevant implications - sql` - SELECT - id, - is_equivalence, - is_deduced, - dualized_from, - proof, - assumptions, - conclusions - FROM category_implications_view - WHERE - EXISTS ( - SELECT 1 - FROM json_each(conclusions) - WHERE value = ${id} - ) - OR - EXISTS ( - SELECT 1 - FROM json_each(assumptions) - WHERE value = ${id} - ) - ORDER BY lower(assumptions) || ' ' || lower(conclusions) - `, - // known categories - sql` - SELECT c.id, c.name, cp.is_satisfied - FROM category_property_assignments cp - INNER JOIN categories c ON c.id = cp.category_id - WHERE cp.property_id = ${id} - ORDER BY lower(c.name) - `, - // unknown categories - sql` - SELECT c.id, c.name - FROM categories c - LEFT JOIN category_property_assignments cp - ON cp.category_id = c.id - AND cp.property_id = ${id} - WHERE - cp.property_id IS NULL - ORDER BY lower(c.name) - `, - ]) + const property_data = fetch_property('category', id) - if (err) error(500, 'Could not load property') - - const [ - properties, - related, - relevant_implications_db, - known_categories, - unknown_categories, - ] = results - - if (!properties.length) error(404, 'Property not found') - - const property = display_property(properties[0]) - - const related_properties = related.map(({ id }) => id) - - const examples = known_categories.filter((c) => c.is_satisfied === 1) - const counterexamples = known_categories.filter((c) => c.is_satisfied === 0) - const undecidable_categories = known_categories.filter((c) => c.is_satisfied === null) - - const relevant_implications = relevant_implications_db.map(display_implication) - - for (const impl of relevant_implications) { - if (!impl.is_equivalence && impl.conclusions.includes(id)) { - impl.conclusions = [id] - } - } - - return render_nested_formulas({ - property, - related_properties, - examples, - counterexamples, - unknown_categories, - undecidable_categories, - relevant_implications, - }) + return render_nested_formulas(property_data) } diff --git a/src/routes/category-property/[id]/+page.svelte b/src/routes/category-property/[id]/+page.svelte index 345cc5797..a031bd741 100644 --- a/src/routes/category-property/[id]/+page.svelte +++ b/src/routes/category-property/[id]/+page.svelte @@ -4,13 +4,4 @@ let { data } = $props() - + diff --git a/src/routes/category-search/+page.server.ts b/src/routes/category-search/+page.server.ts index 2a0ab3c77..1d5908868 100644 --- a/src/routes/category-search/+page.server.ts +++ b/src/routes/category-search/+page.server.ts @@ -1,5 +1,5 @@ -import { get_property_ids } from '$lib/server/properties' +import { get_property_ids } from '$lib/server/fetchers/properties' -export const load = async () => { +export const load = () => { return { all_properties: get_property_ids('category') } } diff --git a/src/routes/category-search/+page.svelte b/src/routes/category-search/+page.svelte index 3d0f99b6e..083471823 100644 --- a/src/routes/category-search/+page.svelte +++ b/src/routes/category-search/+page.svelte @@ -6,7 +6,7 @@ const sample_search_url = `/category-search/results?satisfied=finitely_complete~pointed&unsatisfied=complete` - + Search for categories with certain properties while excluding others. For example, you can look for categories that are finitely complete and pointed but not complete. diff --git a/src/routes/category-search/results/+page.server.ts b/src/routes/category-search/results/+page.server.ts index 9dd8f5783..0646162d4 100644 --- a/src/routes/category-search/results/+page.server.ts +++ b/src/routes/category-search/results/+page.server.ts @@ -1,7 +1,13 @@ -import { search_handler } from '$lib/server/search' +import { fetch_search_results } from '$lib/server/fetchers/search' +import { cache_page } from '$lib/server/utils' export const prerender = false -export const load = async (event) => { - return search_handler(event, 'category') +export const load = (event) => { + const satisfied_query = event.url.searchParams.get('satisfied') + const unsatisfied_query = event.url.searchParams.get('unsatisfied') + + return fetch_search_results(satisfied_query, unsatisfied_query, 'category', () => + cache_page(event), + ) } diff --git a/src/routes/category-search/results/+page.svelte b/src/routes/category-search/results/+page.svelte index b0b140422..44712f45e 100644 --- a/src/routes/category-search/results/+page.svelte +++ b/src/routes/category-search/results/+page.svelte @@ -1,6 +1,7 @@ - + diff --git a/src/routes/category/[id]/+page.server.ts b/src/routes/category/[id]/+page.server.ts index 764d7bdfc..bb30b3b31 100644 --- a/src/routes/category/[id]/+page.server.ts +++ b/src/routes/category/[id]/+page.server.ts @@ -1,178 +1,34 @@ -import { error } from '@sveltejs/kit' import { render_nested_formulas } from '$lib/server/formulas' -import { batch } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' -import type { - PropertyAssignmentDB, - CategoryDisplay, - CommentObject, - PropertyShort, - RelatedStructure, - SpecialMorphism, - SpecialObject, - TagObject, - StructureShort, -} from '$lib/commons/types' -import { display_property_assignment } from '$lib/server/transforms' +import { fetch_structure } from '$lib/server/fetchers/structure' +import { fetch_category } from '$lib/server/fetchers/category' -export const load = async (event) => { +export const load = (event) => { const id = event.params.id - const { results, err } = batch< - [ - CategoryDisplay, - RelatedStructure, - TagObject, - PropertyAssignmentDB, - PropertyShort, - SpecialObject, - SpecialMorphism, - StructureShort, - CommentObject, - ] - >([ - // basic information - sql` - SELECT - c.id, - c.name, - c.notation, - c.objects, - c.morphisms, - c.description, - c.nlab_link, - c.dual_category_id, - d.name AS dual_category_name, - d.notation AS dual_category_notation - FROM categories c - LEFT JOIN categories d ON d.id = c.dual_category_id - WHERE c.id = ${id} - `, - // related categories - sql` - SELECT - r.related_category_id AS id, - c.name, - c.notation - FROM related_categories r - INNER JOIN categories c ON c.id = r.related_category_id - WHERE r.category_id = ${id} - ORDER BY lower(c.name) - `, - // tags - sql` - SELECT ct.tag - FROM category_tag_assignments ct - INNER JOIN category_tags t ON t.tag = ct.tag - WHERE ct.category_id = ${id} - ORDER BY t.id - `, - // properties - sql` - SELECT - cp.property_id AS id, - cp.is_satisfied, - cp.proof, - cp.is_deduced, - p.relation - FROM category_property_assignments cp - INNER JOIN category_properties p ON p.id = cp.property_id - WHERE cp.category_id = ${id} - ORDER BY cp.id - `, - // unknown properties - sql` - SELECT p.id, p.relation - FROM category_properties p - WHERE NOT EXISTS ( - SELECT 1 FROM category_property_assignments - WHERE category_id = ${id} AND property_id = p.id - ) - ORDER BY lower(p.id) - `, - // special objects - sql` - SELECT s.type, s.description - FROM special_objects s - INNER JOIN special_object_types t ON t.type = s.type - WHERE s.category_id = ${id} - ORDER BY t.id - `, - // special morphisms - sql` - SELECT t.type, s.description, s.proof - FROM special_morphism_types t - LEFT JOIN special_morphisms s - ON s.type = t.type AND s.category_id = ${id} - ORDER BY t.id - `, - // undistinguishable categories - sql` - SELECT u.id, u.name - FROM categories u - JOIN category_properties p - LEFT JOIN category_property_assignments cp - ON cp.category_id = ${id} AND cp.property_id = p.id - LEFT JOIN category_property_assignments up - ON up.category_id = u.id AND up.property_id = p.id - WHERE u.id != ${id} - GROUP BY u.id, u.name - HAVING SUM( - CASE - WHEN cp.is_satisfied IS up.is_satisfied THEN 0 - ELSE 1 - END - ) = 0; - `, - // comments - sql` - SELECT id, comment FROM category_comments - WHERE category_id = ${id} - `, - ]) - - if (err) error(500, 'Could not load category') - - const [ - categories, - related_categories, - tag_objects, - properties_db, + const { + structure, + related_structures, + tags, + satisfied_properties, + unsatisfied_properties, unknown_properties, - special_objects, - special_morphisms, - undistinguishable_categories, + undecidable_properties, + undistinguishable_structures, comments, - ] = results - - if (!categories.length) error(404, `Could not find category with ID '${id}'`) - - const category = categories[0] - const tags = tag_objects.map(({ tag }) => tag) - - const satisfied_properties = properties_db - .filter((obj) => obj.is_satisfied === 1) - .map(display_property_assignment) - - const unsatisfied_properties = properties_db - .filter((obj) => obj.is_satisfied === 0) - .map(display_property_assignment) + } = fetch_structure('category', id) - const undecidable_properties = properties_db - .filter((obj) => obj.is_satisfied === null) - .map(display_property_assignment) + const category = fetch_category(id) return render_nested_formulas({ + structure, category, - related_categories, + related_structures, tags, satisfied_properties, unsatisfied_properties, unknown_properties, undecidable_properties, - special_objects, - special_morphisms, - undistinguishable_categories, + undistinguishable_structures, comments, }) } diff --git a/src/routes/category/[id]/+page.svelte b/src/routes/category/[id]/+page.svelte index c38b37c1a..19de4676c 100644 --- a/src/routes/category/[id]/+page.svelte +++ b/src/routes/category/[id]/+page.svelte @@ -1,78 +1,55 @@ - - -

    {data.category.name}

    - - - - - - - -
    -

    Special objects

    - - {#if data.special_objects.length} -
      - {#each data.special_objects as obj} -
    • {obj.type}: {@html obj.description}
      • - {/each} -
    - {:else} -

    —

    - {/if} -
    - -
    -

    Special morphisms

    - -
      - {#each data.special_morphisms as obj} -
    • - - {#if obj.description} - {obj.type}: {@html obj.description} - {:else} - {obj.type}: - {/if} - -
      • - {/each} -
    -
    - - - - - - + + {#snippet definition()} +
  1. + objects: + {@html data.category.objects} +
    2. +
  2. + morphisms: + {@html data.category.morphisms} +
    3. + {/snippet} + + {#snippet specials()} +
    +

    Special objects

    + + {#if data.category.special_objects.length} +
      + {#each data.category.special_objects as obj} +
    • {obj.type}: {@html obj.description}
      • + {/each} +
    + {:else} +

    —

    + {/if} +
    + +
    +

    Special morphisms

    + +
      + {#each data.category.special_morphisms as obj} +
    • + + {#if obj.description} + {obj.type}: {@html obj.description} + {:else} + {obj.type}: + {/if} + +
      • + {/each} +
    +
    + {/snippet} +     diff --git a/src/routes/content/[id]/+page.server.ts b/src/routes/content/[id]/+page.server.ts index 27d3ab111..a2c04ead0 100644 --- a/src/routes/content/[id]/+page.server.ts +++ b/src/routes/content/[id]/+page.server.ts @@ -1,40 +1,14 @@ import { get_rendered_content } from '$lib/server/markdown' import { error } from '@sveltejs/kit' -import { batch } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' -import type { StructureShort, PropertyShort } from '$lib/commons/types' +import { fetch_category_references } from '$lib/server/fetchers/content' -export const load = async (event) => { +export const load = (event) => { const id = event.params.id + const content = get_rendered_content(id) if (!content) error(404, 'Not Found') - const { results, err: err_categories } = batch< - [StructureShort, PropertyShort, { id: string }] - >([ - sql` - SELECT c.id, c.name FROM categories c - WHERE EXISTS ( - SELECT 1 - FROM category_property_assignments cp - WHERE - cp.category_id = c.id - AND cp.proof LIKE '%/content/' || ${id} || '%' - ) - `, - sql` - SELECT id, relation FROM category_properties - WHERE description LIKE '%/content/' || ${id} || '%' - `, - sql` - SELECT id FROM category_implications - WHERE proof LIKE '%/content/' || ${id} || '%' - `, - ]) - - if (err_categories) error(500, 'Could not load context') - - const [categories, category_properties, category_implications] = results + const category_references = fetch_category_references(id) - return { ...content, categories, category_properties, category_implications } + return { ...content, ...category_references } } diff --git a/src/routes/download/+page.svelte b/src/routes/download/+page.svelte index f0a811f44..c8a8736a9 100644 --- a/src/routes/download/+page.svelte +++ b/src/routes/download/+page.svelte @@ -39,8 +39,8 @@ .tables -
    -- Schema of categories table
-.schema categories
+
    -- Schema of structures table
+.schema structures
 
    
 
 
    -- Number of categories
@@ -48,94 +48,101 @@ SELECT COUNT(*) FROM categories;
 
    
 
 
    -- Categories without an nLab link
-SELECT id, name FROM categories WHERE nlab_link IS NULL;
+SELECT id, name FROM structures
+WHERE type = 'category' AND nlab_link IS NULL;
 
    
 
-
    -- Categories involving rings
-SELECT id, name FROM categories WHERE name LIKE '%ring%';
+
    -- Structures involving rings
+SELECT id, name, type FROM structures WHERE name LIKE '%ring%';
 
    
 
 
    -- Finite categories
-SELECT category_id FROM category_property_assignments
-WHERE property_id = 'finite' AND is_satisfied = TRUE;
+SELECT structure_id FROM property_assignments
+WHERE type = 'category' AND property_id = 'finite'
+AND is_satisfied = TRUE;
 
    
 
 
    -- Categories without a generating set
-SELECT category_id FROM category_property_assignments
-WHERE property_id = 'generating set' AND is_satisfied = FALSE;
+SELECT structure_id FROM property_assignments
+WHERE type = 'category' AND property_id = 'generating set'
+AND is_satisfied = FALSE;
 
    
 
 
    -- Abelian categories that are not cocomplete
-SELECT a.category_id
-FROM category_property_assignments a
-CROSS JOIN category_property_assignments b
-WHERE a.category_id = b.category_id
+SELECT a.structure_id
+FROM property_assignments a
+CROSS JOIN property_assignments b
+WHERE a.type = 'category'
+AND a.structure_id = b.structure_id
 AND a.property_id = 'abelian' AND a.is_satisfied = TRUE
 AND b.property_id = 'cocomplete' AND b.is_satisfied = FALSE;
 
    
 
 
    -- Number of categories per tag
-SELECT tag, count(category_id) AS tagged_categories
-FROM category_tag_assignments
+SELECT tag, count(structure_id) AS tagged_categories
+FROM structure_tag_assignments
+WHERE type = 'category'
 GROUP BY tag
 ORDER BY tagged_categories DESC;
 
    
 
 
    -- Properties without a dual
-SELECT id FROM category_properties WHERE dual_property_id IS NULL;
+SELECT id, type FROM properties WHERE dual_property_id IS NULL;
 
    
 
 
    -- Self-dual properties
-SELECT id FROM category_properties WHERE id = dual_property_id;
+SELECT id, type FROM properties WHERE id = dual_property_id;
 
    
 
 
    -- Properties not invariant under equivalences
-SELECT id FROM category_properties WHERE invariant_under_equivalences = FALSE;
+SELECT id, type FROM properties WHERE invariant_under_equivalences = FALSE;
 
    
 
-
    -- Properties without related properties
-SELECT p.id FROM category_properties p
-LEFT JOIN related_category_properties r
+
    -- Properties of categories without related properties
+SELECT p.id FROM properties p
+LEFT JOIN related_properties r
 ON r.property_id = p.id
-WHERE r.related_property_id IS NULL;
+WHERE p.type = 'category' AND r.related_property_id IS NULL;
 
    
 
-
    -- Equivalences
-SELECT assumptions, conclusions FROM category_implications_view
-WHERE is_equivalence = TRUE;
+
    -- Equivalent characterizations
+SELECT assumptions, conclusions FROM implications_view
+WHERE type = 'category' AND is_equivalence = TRUE;
 
    
 
-
    -- Top 5 implications with the most assumptions
-SELECT assumptions, conclusions FROM category_implications_view
+
    -- Top 5 implications of categories with the most assumptions
+SELECT assumptions, conclusions FROM implications_view
+WHERE type = 'category'
 ORDER BY json_array_length(assumptions) DESC LIMIT 5;
 
    
 
 
    -- Trivial proofs
-SELECT category_id, property_id, is_satisfied, proof
-FROM category_property_assignments
+SELECT structure_id, type, property_id, is_satisfied, proof
+FROM property_assignments
 WHERE proof = 'This is trivial.';
 
    
 
 
    -- Top 10 longest proofs
-SELECT category_id, property_id, is_satisfied, proof
-FROM category_property_assignments
+SELECT structure_id, type, property_id, is_satisfied, proof
+FROM property_assignments
 ORDER BY length(proof) DESC LIMIT 10;
 
    
 
 
    -- Top 10 properties with the most undecided categories
-SELECT p.id AS property_id, COUNT(c.id) AS undecided_categories
-FROM category_properties p
-CROSS JOIN categories c
-LEFT JOIN category_property_assignments cp
-ON cp.category_id = c.id AND cp.property_id = p.id
-WHERE cp.property_id IS NULL
+SELECT p.id AS property_id, COUNT(s.id) AS undecided_categories
+FROM properties p
+CROSS JOIN structures s
+LEFT JOIN property_assignments pa
+ON pa.structure_id = s.id AND pa.property_id = p.id
+WHERE p.type = 'category' AND pa.property_id IS NULL
+AND s.type = 'category'
 GROUP BY p.id
 ORDER BY undecided_categories DESC LIMIT 10;
 
    
 
-
    -- Properties which cannot be decided for a given category
-SELECT category_id, property_id, proof
-FROM category_property_assignments
+
    -- Properties which cannot be decided for a given structure
+SELECT structure_id, type, property_id, proof
+FROM property_assignments
 WHERE is_satisfied IS NULL;
 
    
 
diff --git a/src/routes/functor-comparison/+page.server.ts b/src/routes/functor-comparison/+page.server.ts
index 4a4a49f66..b26dc673b 100644
--- a/src/routes/functor-comparison/+page.server.ts
+++ b/src/routes/functor-comparison/+page.server.ts
@@ -1,14 +1,5 @@
-import type { StructureShort } from '$lib/commons/types'
-import sql from 'sql-template-tag'
-import { query } from '$lib/server/db.catdat'
-import { error } from '@sveltejs/kit'
+import { fetch_structures } from '$lib/server/fetchers/structures'
 
-export const load = async () => {
-	const { rows: functors, err } = query(sql`
-		SELECT id, name FROM functors ORDER BY lower(name)
-	`)
-
-	if (err) error(500, 'Functors could not be loaded')
-
-	return { functors }
+export const load = () => {
+	return fetch_structures('functor')
 }
diff --git a/src/routes/functor-comparison/+page.svelte b/src/routes/functor-comparison/+page.svelte
index b2abc1d64..a572a205c 100644
--- a/src/routes/functor-comparison/+page.svelte
+++ b/src/routes/functor-comparison/+page.svelte
@@ -4,4 +4,4 @@
 	let { data } = $props()
 
 
-
+
diff --git a/src/routes/functor-comparison/[...ids]/+page.server.ts b/src/routes/functor-comparison/[...ids]/+page.server.ts
index 9a94f34df..637158805 100644
--- a/src/routes/functor-comparison/[...ids]/+page.server.ts
+++ b/src/routes/functor-comparison/[...ids]/+page.server.ts
@@ -1,7 +1,12 @@
-import { compare_handler } from '$lib/server/compare'
+import { fetch_comparison_result } from '$lib/server/fetchers/comparison'
+import { cache_page } from '$lib/server/utils'
 
 export const prerender = false
 
-export const load = async (event) => {
-	return compare_handler(event, 'functor')
+export const load = (event) => {
+	const compared_ids = event.params.ids.split('/')
+
+	return fetch_comparison_result(compared_ids, 'functor', () => {
+		cache_page(event)
+	})
 }
diff --git a/src/routes/functor-comparison/[...ids]/+page.svelte b/src/routes/functor-comparison/[...ids]/+page.svelte
index bc78c0081..e942fb34b 100644
--- a/src/routes/functor-comparison/[...ids]/+page.svelte
+++ b/src/routes/functor-comparison/[...ids]/+page.svelte
@@ -4,4 +4,4 @@
 	let { data } = $props()
 
 
-
+
diff --git a/src/routes/functor-implication/[id]/+page.server.ts b/src/routes/functor-implication/[id]/+page.server.ts
index f87e6d65c..8136bece3 100644
--- a/src/routes/functor-implication/[id]/+page.server.ts
+++ b/src/routes/functor-implication/[id]/+page.server.ts
@@ -1,45 +1,8 @@
+import { fetch_implication } from '$lib/server/fetchers/implication'
 import { render_nested_formulas } from '$lib/server/formulas'
-import { batch } from '$lib/server/db.catdat'
-import sql from 'sql-template-tag'
-import { error } from '@sveltejs/kit'
-import type { ImplicationDB, StructureShort } from '$lib/commons/types'
-import { display_implication } from '$lib/server/transforms'
 
-export const load = async (event) => {
+export const load = (event) => {
 	const id = event.params.id
 
-	const { results, err } = batch<[ImplicationDB, StructureShort]>([
-		sql`
-            SELECT
-                id,
-                is_equivalence,
-                is_deduced,
-                dualized_from,
-                proof,
-                assumptions,
-                conclusions,
-                source_assumptions,
-                target_assumptions
-            FROM functor_implications_view
-            WHERE id = ${id}
-        `,
-		sql`
-            SELECT f.id, f.name FROM functors f
-            WHERE EXISTS (
-                SELECT 1 FROM functor_property_assignments fp
-                WHERE fp.functor_id = f.id
-                AND fp.proof LIKE '%/functor-implication/' || ${id} || '%'
-            )
-        `,
-	])
-
-	if (err) error(500, 'Could not load implication')
-
-	const [implications, functors] = results
-
-	if (!implications.length) error(404, `Could not find implication with ID '${id}'`)
-
-	const implication = display_implication(implications[0])
-
-	return render_nested_formulas({ implication, functors })
+	return render_nested_formulas(fetch_implication('functor', id))
 }
diff --git a/src/routes/functor-implication/[id]/+page.svelte b/src/routes/functor-implication/[id]/+page.svelte
index 837875d0a..e3588dd4e 100644
--- a/src/routes/functor-implication/[id]/+page.svelte
+++ b/src/routes/functor-implication/[id]/+page.svelte
@@ -1,11 +1,7 @@
 
 
-
+
diff --git a/src/routes/functor-implications/+page.server.ts b/src/routes/functor-implications/+page.server.ts
index 6559e6a25..b234154c8 100644
--- a/src/routes/functor-implications/+page.server.ts
+++ b/src/routes/functor-implications/+page.server.ts
@@ -1,29 +1,8 @@
 import { render_nested_formulas } from '$lib/server/formulas'
-import { query } from '$lib/server/db.catdat'
-import sql from 'sql-template-tag'
-import { error } from '@sveltejs/kit'
-import type { ImplicationDB } from '$lib/commons/types'
-import { display_implication } from '$lib/server/transforms'
+import { fetch_implications } from '$lib/server/fetchers/implications'
 
-export const load = async () => {
-	const { rows, err } = query(sql`
-        SELECT
-            id,
-            is_equivalence,
-            is_deduced,
-            dualized_from,
-            proof,
-            assumptions,
-            conclusions,
-            source_assumptions,
-            target_assumptions
-        FROM functor_implications_view
-        ORDER BY lower(assumptions) || ' ' || lower(conclusions)
-    `)
-
-	if (err) error(500, 'Could not load implications')
-
-	const implications = rows.map(display_implication)
+export const load = () => {
+	const { implications } = fetch_implications('functor')
 
 	return render_nested_formulas({ implications })
 }
diff --git a/src/routes/functor-properties/+page.server.ts b/src/routes/functor-properties/+page.server.ts
index de80fe08b..6635d2729 100644
--- a/src/routes/functor-properties/+page.server.ts
+++ b/src/routes/functor-properties/+page.server.ts
@@ -1,44 +1,5 @@
-import type { GroupedPropertyShort } from '$lib/commons/types'
-import { query } from '$lib/server/db.catdat'
-import { error } from '@sveltejs/kit'
-import sql from 'sql-template-tag'
+import { get_grouped_properties } from '$lib/server/fetchers/properties'
 
-// TODO: remove code duplication with category properties list page
-
-export const load = async () => {
-	const { rows: properties, err } = query(sql`
-        SELECT id, relation, dual_property_id FROM functor_properties
-        ORDER BY lower(id)
-    `)
-
-	if (err) error(500, 'Could not load properties')
-
-	const seen = new Set()
-
-	const grouped_properties: typeof properties = []
-
-	for (const p of properties) {
-		if (seen.has(p.id) || (p.dual_property_id && seen.has(p.dual_property_id))) {
-			continue
-		}
-
-		if (p.id.startsWith('co') && p.dual_property_id) {
-			const swap = {
-				id: p.dual_property_id,
-				dual_property_id: p.id,
-				relation: p.relation,
-			}
-			grouped_properties.push(swap)
-		} else {
-			grouped_properties.push(p)
-		}
-
-		seen.add(p.id)
-		if (p.dual_property_id) seen.add(p.dual_property_id)
-	}
-
-	const total = properties.length
-	const grouped_total = grouped_properties.length
-
-	return { grouped_properties, total, grouped_total }
+export const load = () => {
+	return get_grouped_properties('functor')
 }
diff --git a/src/routes/functor-properties/+page.svelte b/src/routes/functor-properties/+page.svelte
index b9ab8b415..3e22335dd 100644
--- a/src/routes/functor-properties/+page.svelte
+++ b/src/routes/functor-properties/+page.svelte
@@ -1,5 +1,6 @@
 
 
diff --git a/src/routes/functor-property/[id]/+page.server.ts b/src/routes/functor-property/[id]/+page.server.ts
index dc13e9c9e..b08c10122 100644
--- a/src/routes/functor-property/[id]/+page.server.ts
+++ b/src/routes/functor-property/[id]/+page.server.ts
@@ -1,126 +1,11 @@
-import { decode_property_ID } from '$lib/commons/property.url'
-import type { ImplicationDB, StructureShort, PropertyDB } from '$lib/commons/types'
-import { batch } from '$lib/server/db.catdat'
 import { render_nested_formulas } from '$lib/server/formulas'
-import { display_implication, display_property } from '$lib/server/transforms'
-import { error } from '@sveltejs/kit'
-import sql from 'sql-template-tag'
+import { decode_property_ID } from '$lib/commons/property.url'
+import { fetch_property } from '$lib/server/fetchers/property'
 
-export const load = async (event) => {
+export const load = (event) => {
 	const id = decode_property_ID(event.params.id)
 
-	const { results, err } = batch<
-		[
-			PropertyDB,
-			{ id: string },
-			ImplicationDB,
-			StructureShort & { is_satisfied: 0 | 1 | null },
-			StructureShort,
-		]
-	>([
-		// basic information
-		sql`
-            SELECT
-                id,
-                relation,
-                description,
-                dual_property_id,
-                nlab_link,
-                invariant_under_equivalences
-            FROM
-                functor_properties
-            WHERE id = ${id}
-        `,
-		// related properties
-		sql`
-            SELECT related_property_id AS id
-            FROM related_functor_properties
-            WHERE property_id = ${id}
-            ORDER BY lower(id)
-        `,
-		// relevant implications
-		sql`
-            SELECT
-                id,
-                is_equivalence,
-                is_deduced,
-                dualized_from,
-                proof,
-                assumptions,
-                source_assumptions,
-                target_assumptions,
-                conclusions
-            FROM functor_implications_view
-            WHERE
-                EXISTS (
-                    SELECT 1
-                    FROM json_each(conclusions)
-                    WHERE value = ${id}
-                )
-                OR
-                EXISTS (
-                    SELECT 1
-                    FROM json_each(assumptions)
-                    WHERE value = ${id}
-                )
-            ORDER BY lower(assumptions) || ' ' || lower(conclusions)
-        `,
-		// known functors
-		sql`
-            SELECT f.id, f.name, fp.is_satisfied
-            FROM functor_property_assignments fp
-            INNER JOIN functors f ON f.id = fp.functor_id
-            WHERE fp.property_id = ${id}
-            ORDER BY lower(f.name)
-        `,
-		// unknown functors
-		sql`
-            SELECT f.id, f.name
-            FROM functors f
-            LEFT JOIN functor_property_assignments fp
-                ON fp.functor_id = f.id
-                AND fp.property_id = ${id}
-            WHERE
-                fp.property_id IS NULL
-            ORDER BY lower(f.name)
-        `,
-	])
-
-	if (err) error(500, 'Could not load properties')
-
-	const [
-		properties,
-		related,
-		relevant_implications_db,
-		known_functors,
-		unknown_functors,
-	] = results
-
-	if (!properties.length) error(404, 'Property not found')
-
-	const property = display_property(properties[0])
-
-	const related_properties = related.map(({ id }) => id)
-
-	const examples = known_functors.filter((f) => f.is_satisfied === 1)
-	const counterexamples = known_functors.filter((f) => f.is_satisfied === 0)
-	const undecidable_functors = known_functors.filter((f) => f.is_satisfied === null)
-
-	const relevant_implications = relevant_implications_db.map(display_implication)
-
-	for (const impl of relevant_implications) {
-		if (!impl.is_equivalence && impl.conclusions.includes(id)) {
-			impl.conclusions = [id]
-		}
-	}
+	const property_data = fetch_property('functor', id)
 
-	return render_nested_formulas({
-		property,
-		related_properties,
-		examples,
-		counterexamples,
-		unknown_functors,
-		undecidable_functors,
-		relevant_implications,
-	})
+	return render_nested_formulas(property_data)
 }
diff --git a/src/routes/functor-property/[id]/+page.svelte b/src/routes/functor-property/[id]/+page.svelte
index b436a51a7..5ac5a3d01 100644
--- a/src/routes/functor-property/[id]/+page.svelte
+++ b/src/routes/functor-property/[id]/+page.svelte
@@ -4,13 +4,4 @@
 	let { data } = $props()
 
 
-
+
diff --git a/src/routes/functor-search/+page.server.ts b/src/routes/functor-search/+page.server.ts
index bc77cc3fe..6aa4f890b 100644
--- a/src/routes/functor-search/+page.server.ts
+++ b/src/routes/functor-search/+page.server.ts
@@ -1,5 +1,5 @@
-import { get_property_ids } from '$lib/server/properties'
+import { get_property_ids } from '$lib/server/fetchers/properties'
 
-export const load = async () => {
+export const load = () => {
 	return { all_properties: get_property_ids('functor') }
 }
diff --git a/src/routes/functor-search/+page.svelte b/src/routes/functor-search/+page.svelte
index cbf217ef1..e174c391d 100644
--- a/src/routes/functor-search/+page.svelte
+++ b/src/routes/functor-search/+page.svelte
@@ -6,7 +6,7 @@
 	const sample_search_url = `/functor-search/results?satisfied=continuous&unsatisfied=cocontinuous`
 
 
-
+
 	Search for functors with certain properties while excluding others. For example, you
 	can look for functors that are continuous but not cocontinuous.
 
diff --git a/src/routes/functor-search/results/+page.server.ts b/src/routes/functor-search/results/+page.server.ts
index 624bf3555..d5acdfd57 100644
--- a/src/routes/functor-search/results/+page.server.ts
+++ b/src/routes/functor-search/results/+page.server.ts
@@ -1,7 +1,13 @@
-import { search_handler } from '$lib/server/search'
+import { fetch_search_results } from '$lib/server/fetchers/search'
+import { cache_page } from '$lib/server/utils'
 
 export const prerender = false
 
-export const load = async (event) => {
-	return search_handler(event, 'functor')
+export const load = (event) => {
+	const satisfied_query = event.url.searchParams.get('satisfied')
+	const unsatisfied_query = event.url.searchParams.get('unsatisfied')
+
+	return fetch_search_results(satisfied_query, unsatisfied_query, 'functor', () =>
+		cache_page(event),
+	)
 }
diff --git a/src/routes/functor-search/results/+page.svelte b/src/routes/functor-search/results/+page.svelte
index b0b140422..44516cde3 100644
--- a/src/routes/functor-search/results/+page.svelte
+++ b/src/routes/functor-search/results/+page.svelte
@@ -1,6 +1,7 @@
 
 
-
+
diff --git a/src/routes/functor/[id]/+page.server.ts b/src/routes/functor/[id]/+page.server.ts
index 8cdfacfc6..a85ddf339 100644
--- a/src/routes/functor/[id]/+page.server.ts
+++ b/src/routes/functor/[id]/+page.server.ts
@@ -1,182 +1,34 @@
-import type {
-	CommentObject,
-	FunctorDisplay,
-	PropertyAssignmentDB,
-	PropertyShort,
-	RelatedStructure,
-	StructureShort,
-	TagObject,
-} from '$lib/commons/types'
-import { batch } from '$lib/server/db.catdat'
+import { fetch_functor } from '$lib/server/fetchers/functor'
+import { fetch_structure } from '$lib/server/fetchers/structure'
 import { render_nested_formulas } from '$lib/server/formulas'
-import { display_property_assignment } from '$lib/server/transforms'
-import { error } from '@sveltejs/kit'
-import sql from 'sql-template-tag'
 
-// TODO: remove code duplication with category detail page
-
-export const load = async (event) => {
+export const load = (event) => {
 	const id = event.params.id
 
-	const { results, err } = batch<
-		[
-			FunctorDisplay,
-			RelatedStructure,
-			RelatedStructure,
-			RelatedStructure,
-			TagObject,
-			PropertyAssignmentDB,
-			PropertyShort,
-			StructureShort,
-			CommentObject,
-		]
-	>([
-		// basic information
-		sql`
-            SELECT
-                f.id,
-				f.name,
-				f.notation,
-				f.source,
-				f.target,
-				f.description,
-				f.nlab_link,
-                s.name AS source_name,
-				t.name AS target_name,
-				s.notation AS source_notation,
-				t.notation AS target_notation
-            FROM functors f
-            INNER JOIN categories s ON s.id = f.source
-            INNER JOIN categories t ON t.id = f.target
-            WHERE f.id = ${id}
-        `,
-		// related functors
-		sql`
-			SELECT
-				r.related_functor_id AS id,
-				f.name,
-				f.notation
-			FROM related_functors r
-			INNER JOIN functors f ON f.id = r.related_functor_id
-			WHERE r.functor_id = ${id}
-			ORDER BY lower(f.name)
-		`,
-		// left adjoint functor
-		sql`
-			SELECT f.id, f.name, f.notation
-			FROM adjoint_functors a
-			INNER JOIN functors f ON f.id = a.left_adjoint
-			WHERE a.right_adjoint = ${id}
-		`,
-		// right adjoint functor
-		sql`
-			SELECT f.id, f.name, f.notation
-			FROM adjoint_functors a
-			INNER JOIN functors f ON f.id = a.right_adjoint
-			WHERE a.left_adjoint = ${id}
-		`,
-		// tags
-		sql`
-			SELECT ft.tag
-			FROM functor_tag_assignments ft
-			INNER JOIN functor_tags t ON t.tag = ft.tag
-			WHERE ft.functor_id = ${id}
-			ORDER BY t.id
-		`,
-		// properties
-		sql`
-			SELECT
-				fp.property_id AS id,
-				fp.is_satisfied,
-				fp.proof,
-				fp.is_deduced,
-				p.relation
-			FROM functor_property_assignments fp
-			INNER JOIN functor_properties p ON p.id = fp.property_id
-			WHERE fp.functor_id = ${id}
-			ORDER BY fp.id
-		`,
-		// unknown properties
-		sql`
-			SELECT p.id, p.relation
-			FROM functor_properties p
-			WHERE NOT EXISTS (
-				SELECT 1 FROM functor_property_assignments
-				WHERE functor_id = ${id} AND property_id = p.id
-			)
-			ORDER BY lower(p.id)
-		`,
-		// undistinguishable functors
-		sql`
-			SELECT u.id, u.name
-			FROM functors u
-			JOIN functor_properties p
-			LEFT JOIN functor_property_assignments fp
-				ON fp.functor_id = ${id} AND fp.property_id = p.id
-			LEFT JOIN functor_property_assignments up
-				ON up.functor_id = u.id AND up.property_id = p.id
-			WHERE u.id != ${id}
-			GROUP BY u.id, u.name
-			HAVING SUM(
-				CASE
-					WHEN fp.is_satisfied IS up.is_satisfied THEN 0
-					ELSE 1
-				END
-			) = 0;
-		`,
-		// comments
-		sql`
-			SELECT id, comment FROM functor_comments
-			WHERE functor_id = ${id}
-		`,
-	])
-
-	if (err) error(500, 'Could not load functor')
-
-	const [
-		functors,
-		related_functors,
-		left_adjoints,
-		right_adjoints,
-		tag_objects,
-		properties_db,
+	const {
+		structure,
+		related_structures,
+		tags,
+		satisfied_properties,
+		unsatisfied_properties,
 		unknown_properties,
-		undistinguishable_functors,
+		undecidable_properties,
+		undistinguishable_structures,
 		comments,
-	] = results
-
-	if (!functors.length) error(404, `Could not find functor with ID '${id}'`)
-
-	const functor = functors[0]
-
-	const left_adjoint = left_adjoints.at(0)
-	const right_adjoint = right_adjoints.at(0)
-
-	const tags = tag_objects.map(({ tag }) => tag)
-
-	const satisfied_properties = properties_db
-		.filter((obj) => obj.is_satisfied === 1)
-		.map(display_property_assignment)
-
-	const unsatisfied_properties = properties_db
-		.filter((obj) => obj.is_satisfied === 0)
-		.map(display_property_assignment)
+	} = fetch_structure('functor', id)
 
-	const undecidable_properties = properties_db
-		.filter((obj) => obj.is_satisfied === null)
-		.map(display_property_assignment)
+	const functor = fetch_functor(id)
 
 	return render_nested_formulas({
+		structure,
 		functor,
-		related_functors,
-		left_adjoint,
-		right_adjoint,
+		related_structures,
 		tags,
 		satisfied_properties,
 		unsatisfied_properties,
 		unknown_properties,
 		undecidable_properties,
-		undistinguishable_functors,
+		undistinguishable_structures,
 		comments,
 	})
 }
diff --git a/src/routes/functor/[id]/+page.svelte b/src/routes/functor/[id]/+page.svelte
index cf3973169..5b7bc43d9 100644
--- a/src/routes/functor/[id]/+page.svelte
+++ b/src/routes/functor/[id]/+page.svelte
@@ -1,45 +1,43 @@
 
 
-
-
-
    {data.functor.name}
    
-
-
-
-
-
-
-
-
-
-
-
-
+
+	{#snippet definition()}
+		
  3. 
+			Source:
+			{data.functor.source_name}
+		
    4. 
+
+		
  4. 
+			Target:
+			{data.functor.target_name}
+		
    5. 
+
+		{#if data.functor.left_adjoint}
+			
  5. 
+				Left adjoint:
+				
+					{@html data.functor.left_adjoint_notation}
+				
+			
    6. 
+		{/if}
+
+		{#if data.functor.right_adjoint}
+			
  6. 
+				Right adjoint:
+				
+					{@html data.functor.right_adjoint_notation}
+				
+			
    7. 
+		{/if}
+	{/snippet}
+    
diff --git a/src/routes/functors/+page.server.ts b/src/routes/functors/+page.server.ts
index 0b25908d4..77c00b6ce 100644
--- a/src/routes/functors/+page.server.ts
+++ b/src/routes/functors/+page.server.ts
@@ -1,19 +1,5 @@
-import type { StructureShort, TagObject } from '$lib/commons/types'
-import { batch } from '$lib/server/db.catdat'
-import { error } from '@sveltejs/kit'
-import sql from 'sql-template-tag'
+import { fetch_structures_and_tags } from '$lib/server/fetchers/structures'
 
-export const load = async () => {
-	const { results, err } = batch<[StructureShort, TagObject]>([
-		sql`SELECT id, name FROM functors ORDER BY lower(name)`,
-		sql`SELECT tag FROM functor_tags ORDER BY id`,
-	])
-
-	if (err) error(500, 'Functors could not be loaded')
-
-	const [functors, tag_objects] = results
-
-	const tags = tag_objects.map(({ tag }) => tag)
-
-	return { functors, tags }
+export const load = () => {
+	return fetch_structures_and_tags('functor')
 }
diff --git a/src/routes/functors/+page.svelte b/src/routes/functors/+page.svelte
index d66d1ec04..6ab1832de 100644
--- a/src/routes/functors/+page.svelte
+++ b/src/routes/functors/+page.svelte
@@ -4,4 +4,4 @@
 	let { data } = $props()
 
 
-
+
diff --git a/src/routes/functors/[tag]/+page.server.ts b/src/routes/functors/[tag]/+page.server.ts
index bd576a39e..7c7b5dec9 100644
--- a/src/routes/functors/[tag]/+page.server.ts
+++ b/src/routes/functors/[tag]/+page.server.ts
@@ -1,26 +1,12 @@
-import type { StructureShort, TagObject } from '$lib/commons/types'
-import { query } from '$lib/server/db.catdat'
-import { error } from '@sveltejs/kit'
-import sql from 'sql-template-tag'
 import type { EntryGenerator } from './$types'
+import { fetch_tagged_structures } from '$lib/server/fetchers/structures'
+import { fetch_tags } from '$lib/server/fetchers/tags'
 
-export const entries: EntryGenerator = async () => {
-	const { rows, err } = query(sql`SELECT tag FROM functor_tags`)
-	if (err) throw new Error('Database error: Failed to load tags')
-	return rows
+export const entries: EntryGenerator = () => {
+	return fetch_tags('functor')
 }
 
-export const load = async (event) => {
+export const load = (event) => {
 	const tag = event.params.tag
-
-	const { rows: functors, err } = query(sql`
-		SELECT f.id, f.name FROM functors f
-		LEFT JOIN functor_tag_assignments t ON f.id = t.functor_id
-		WHERE t.tag = ${tag}
-		ORDER BY lower(name)
-	`)
-
-	if (err) error(500, 'Functors could not be loaded')
-
-	return { functors, tag }
+	return fetch_tagged_structures('functor', tag)
 }
diff --git a/src/routes/functors/[tag]/+page.svelte b/src/routes/functors/[tag]/+page.svelte
index bb62c7cdd..aa765c464 100644
--- a/src/routes/functors/[tag]/+page.svelte
+++ b/src/routes/functors/[tag]/+page.svelte
@@ -4,4 +4,4 @@
 	let { data } = $props()
 
 
-
+
diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts
index bc139eaed..7017258ef 100644
--- a/src/routes/missing/+page.server.ts
+++ b/src/routes/missing/+page.server.ts
@@ -1,144 +1,28 @@
-import { batch } from '$lib/server/db.catdat'
-import sql from 'sql-template-tag'
-import type { StructureShort } from '$lib/commons/types'
-import { error } from '@sveltejs/kit'
-import { get_missing_combinations } from '$lib/server/consistency'
+import { fetch_missing_data } from '$lib/server/fetchers/missing_data'
+import { fetch_categories_with_missing_morphisms } from '$lib/server/fetchers/category'
 
-type StructurePair = { id1: string; name1: string; id2: string; name2: string }
+export const load = () => {
+	const categories_with_missing_morphisms = fetch_categories_with_missing_morphisms()
 
-export const load = async () => {
-	const { results, err } = batch<
-		[
-			StructureShort & { count: number },
-			StructureShort & { count: number },
-			StructureShort & { count: number },
-			StructurePair,
-			StructurePair,
-		]
-	>([
-		// categories with unknown properties
-		sql`
-			SELECT c.id, c.name, COUNT(*) AS count
-			FROM categories c
-			INNER JOIN category_properties p
-			LEFT JOIN category_property_assignments cp
-				ON cp.category_id = c.id
-				AND cp.property_id = p.id
-			WHERE cp.property_id IS NULL
-			GROUP BY c.id
-			ORDER BY lower(c.name);
-		`,
-		// functors with unknown properties
-		sql`
-			SELECT f.id, f.name, COUNT(*) AS count
-			FROM functors f
-			INNER JOIN functor_properties p
-			LEFT JOIN functor_property_assignments fp
-				ON fp.functor_id = f.id
-				AND fp.property_id = p.id
-			WHERE fp.property_id IS NULL
-			GROUP BY f.id
-			ORDER BY lower(f.name);
-		`,
-		// categories with missing special morphisms
-		sql`
-			SELECT c.id, c.name, COUNT(*) AS count
-			FROM categories c
-			JOIN special_morphism_types t
-			LEFT JOIN special_morphisms s
-				ON s.category_id = c.id AND s.type = t.type
-			WHERE s.type IS NULL
-			GROUP BY c.id
-			ORDER BY lower(c.name);
-		`,
-		// undistinguishable category pairs
-		sql`
-			SELECT
-				c1.id AS id1, c1.name AS name1,
-				c2.id AS id2, c2.name AS name2
-			FROM categories c1
-			JOIN categories c2
-				ON c1.id < c2.id
-			JOIN category_properties p
-			LEFT JOIN category_property_assignments a1
-				ON a1.category_id = c1.id AND a1.property_id = p.id
-			LEFT JOIN category_property_assignments a2
-				ON a2.category_id = c2.id AND a2.property_id = p.id
-			GROUP BY c1.id, c1.name, c2.id, c2.name
-			HAVING SUM(
-			CASE
-				WHEN a1.is_satisfied IS a2.is_satisfied THEN 0
-				ELSE 1
-			END
-			) = 0;
-		`,
-		// undistinguishable functor pairs
-		sql`
-			SELECT
-				f1.id AS id1, f1.name AS name1,
-				f2.id AS id2, f2.name AS name2
-			FROM functors f1
-			JOIN functors f2
-				ON f1.id < f2.id
-			JOIN functor_properties p
-			LEFT JOIN functor_property_assignments a1
-				ON a1.functor_id = f1.id AND a1.property_id = p.id
-			LEFT JOIN functor_property_assignments a2
-				ON a2.functor_id = f2.id AND a2.property_id = p.id
-			GROUP BY f1.id, f1.name, f2.id, f2.name
-			HAVING SUM(
-			CASE
-				WHEN a1.is_satisfied IS a2.is_satisfied THEN 0
-				ELSE 1
-			END
-			) = 0;
-		`,
-	])
-
-	if (err) error(500, 'Failed to load data')
-
-	const [
-		categories_with_unknown_properties,
-		functors_with_unknown_properties,
-		categories_with_missing_morphisms,
-		undistinguishable_category_pairs,
-		undistinguishable_functor_pairs,
-	] = results
-
-	const total_unknown_category_property_pairs =
-		categories_with_unknown_properties.reduce((total, item) => item.count + total, 0)
-
-	const total_unknown_functor_property_pairs = functors_with_unknown_properties.reduce(
-		(total, item) => item.count + total,
-		0,
-	)
-
-	const { missing_combinations: missing_category_combinations, err: err_cat_missing } =
-		get_missing_combinations('category')
-
-	if (err_cat_missing) error(500, 'Failed to load missing category combinations')
-
-	const { missing_combinations: missing_functor_combinations, err: err_fun_missing } =
-		get_missing_combinations('functor')
-
-	if (err_fun_missing) error(500, 'Failed to load missing functor combinations')
+	const missing_category_data = fetch_missing_data('category')
+	const missing_functor_data = fetch_missing_data('functor')
 
 	return {
 		structures_with_unknown_properties: {
-			category: categories_with_unknown_properties,
-			functor: functors_with_unknown_properties,
+			category: missing_category_data.structures_with_unknown_properties,
+			functor: missing_functor_data.structures_with_unknown_properties,
 		},
 		unknown_totals: {
-			category: total_unknown_category_property_pairs,
-			functor: total_unknown_functor_property_pairs,
+			category: missing_category_data.total_unknown_property_pairs,
+			functor: missing_functor_data.total_unknown_property_pairs,
 		},
 		undistinguishable_pairs: {
-			category: undistinguishable_category_pairs,
-			functor: undistinguishable_functor_pairs,
+			category: missing_category_data.undistinguishable_structure_pairs,
+			functor: missing_functor_data.undistinguishable_structure_pairs,
 		},
 		missing_combinations: {
-			category: missing_category_combinations,
-			functor: missing_functor_combinations,
+			category: missing_category_data.missing_combinations,
+			functor: missing_functor_data.missing_combinations,
 		},
 		categories_with_missing_morphisms,
 	}