Skip to content

Latest commit

 

History

History
117 lines (69 loc) · 3.97 KB

DATABASE.md

File metadata and controls

117 lines (69 loc) · 3.97 KB

The database of CatDat

Overview

CatDat is based on a SQLite database. During runtime of the application, it is read-only.

The local copy of the database is located at /database/catdat.db. It contains three main tables:

  • structures
  • properties
  • implications

The structures table stores data that is common to all types of categorical structures. These types are currently supported: categories, functors, morphisms, and symmetric monoidal categories. They are stored in the following table:

  • structure_types

Properties (whether satisfied or not) are associated with categorical structures via the following table:

  • property_assignments

To mark properties as assumptions or conclusions of an implication, there are two tables:

  • assumptions
  • conclusions

These tables are abstracted through the implications_view view.

Functor implications may also depend on properties of the domain or codomain category. Likewise, morphism implications may depend on properties of the ambient category. Such dependencies are stored in the following table:

  • associated_assumptions

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 /database/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 are defined in YAML files located in the subfolder /database/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.

For text-only changes to existing structures, properties, and implications, use

pnpm db:text

This compares the YAML text with the existing database and updates changed texts (such as descriptions and proofs) without changing relations or running deductions. Pass --watch to keep the command running and update whenever a YAML file changes.

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.

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 that verify that the data behaves as expected.

One command for everything

Use the command

pnpm db:update

to run all the commands in sequence: pnpm db:sort (which sorts the JSON files used by the tests), pnpm db:seed, pnpm db:deduce, and pnpm db:test. This also creates a copy of the local database in the /static folder.

Pass --watch to rerun the update whenever a file in the data folder changes:

pnpm db:update --watch

While pnpm dev is running, the browser reloads automatically after pnpm db:update or pnpm db:text has changed the database.

Properties of a structure

Use the command

pnpm db:structure <structure-id> [group]

to list the satisfied, unsatisfied, unknown, and undecidable properties of a structure in the terminal, grouped as on its detail page. Pass one of these groups as a second argument to list only that group.

Diagram

This is the database schema as of 25.10.2026; changes may occur.

database diagram