Minor database improvements

DATABASE.md

@@ -105,4 +105,4 @@ to check for redundant assignments of properties to categorical structures.
 
 This is the database schema as of 18.09.2026; changes may occur.
 
-<img alt="database diagram" src="https://github.com/user-attachments/assets/31a8e7f3-59b0-4d57-8d06-0aa554e8159a" />
+<img alt="database diagram" src="https://github.com/user-attachments/assets/053744e9-71c4-4fb5-82a1-8cdd3bbea3e2" />

database/data/config.yaml

@@ -82,24 +82,24 @@ relations:
     negation: does not preserve
     conditional: would preserve
 
-special_object_types:
-  - type: terminal object
+special_objects:
+  - kind: terminal object
     dual: initial object
-  - type: initial object
+  - kind: initial object
     dual: terminal object
-  - type: products
+  - kind: products
     dual: coproducts
-  - type: coproducts
+  - kind: coproducts
     dual: products
 
-special_morphism_types:
-  - type: isomorphisms
+special_morphisms:
+  - kind: isomorphisms
     dual: isomorphisms
-  - type: monomorphisms
+  - kind: monomorphisms
     dual: epimorphisms
-  - type: epimorphisms
+  - kind: epimorphisms
     dual: monomorphisms
-  - type: regular monomorphisms
+  - kind: regular monomorphisms
     dual: regular epimorphisms
-  - type: regular epimorphisms
+  - kind: regular epimorphisms
     dual: regular monomorphisms

database/data/special-morphism-rules.yaml

@@ -1,84 +1,84 @@
 - property: groupoid
-  type: isomorphisms
+  kind: isomorphisms
   description: every morphism
   proof: The category is a groupoid.
 
 - property: gaunt
-  type: isomorphisms
+  kind: isomorphisms
   description: only the identities
   proof: The category is gaunt.
 
 - property: thin
-  type: monomorphisms
+  kind: monomorphisms
   description: every morphism
   proof: It is a thin category.
 
 - property: thin
-  type: epimorphisms
+  kind: epimorphisms
   description: every morphism
   proof: It is a thin category.
 
 - property: left cancellative
-  type: monomorphisms
+  kind: monomorphisms
   description: every morphism
   proof: The category is left cancellative.
 
 - property: right cancellative
-  type: epimorphisms
+  kind: epimorphisms
   description: every morphism
   proof: The category is right cancellative.
 
 - property: left cancellative
-  type: regular epimorphisms
+  kind: regular epimorphisms
   description: same as isomorphisms
   proof: The category is left cancellative, and a regular epimorphism which is a monomorphism must be an isomorphism.
 
 - property: right cancellative
-  type: regular monomorphisms
+  kind: regular monomorphisms
   description: same as isomorphisms
   proof: The category is right cancellative, and a regular monomorphism which is an epimorphism must be an isomorphism.
 
 - property: one-sorted finitary algebraic
-  type: isomorphisms
+  kind: isomorphisms
   description: bijective morphisms
   proof: 'This holds in every one-sorted finitary algebraic category: the inverse of a bijective morphism is again a morphism.'
 
 - property: one-sorted finitary algebraic
-  type: monomorphisms
+  kind: monomorphisms
   description: injective morphisms
   proof: 'This holds in every one-sorted finitary algebraic category: the forgetful functor to sets is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'
 
 - property: one-sorted finitary algebraic
-  type: regular epimorphisms
+  kind: regular epimorphisms
   description: surjective morphisms
   proof: 'This holds in every one-sorted finitary algebraic category: the construction of coequalizers shows that every regular epimorphism is surjective. Conversely, the fundamental theorem on homomorphisms states that every surjective homomorphism $A \to B$ is the coequalizer of the two projections $A \times_B A \rightrightarrows A$.'
 
 - property: mono-regular
-  type: regular monomorphisms
+  kind: regular monomorphisms
   description: same as monomorphisms
   proof: The category is mono-regular.
 
 - property: epi-regular
-  type: regular epimorphisms
+  kind: regular epimorphisms
   description: same as epimorphisms
   proof: The category is epi-regular.
 
 - property: subobject-trivial
-  type: monomorphisms
+  kind: monomorphisms
   description: same as isomorphisms
   proof: The category is subobject-trivial.
 
 - property: quotient-trivial
-  type: epimorphisms
+  kind: epimorphisms
   description: same as isomorphisms
   proof: The category is quotient-trivial.
 
 - property: regular-subobject-trivial
-  type: regular monomorphisms
+  kind: regular monomorphisms
   description: same as isomorphisms
   proof: The category is regular-subobject-trivial.
 
 - property: regular-quotient-trivial
-  type: regular epimorphisms
+  kind: regular epimorphisms
   description: same as isomorphisms
   proof: The category is regular-quotient-trivial.

database/schema/001_structures.sql

@@ -8,29 +8,6 @@ INSERT INTO structure_types (type) VALUES
     ('morphism'),
     ('symmetric_monoidal_category');
 
-
-CREATE TABLE associated_structure_types (
-    label TEXT NOT NULL,
-    type TEXT NOT NULL,
-    associated_type TEXT NOT NULL,
-    required INTEGER NOT NULL
-         CHECK (required in (TRUE, FALSE)),
-    PRIMARY KEY (label, type, associated_type),
-    UNIQUE (label, type),
-    FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE,
-    FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE
-);
-
-INSERT INTO associated_structure_types
-    (label, type, associated_type, required)
-VALUES
-    ('domain', 'functor', 'category', TRUE),
-    ('codomain', 'functor', 'category', TRUE),
-    ('category', 'morphism', 'category', TRUE),
-    ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE),
-    ('left_adjoint', 'functor', 'functor', FALSE),
-    ('right_adjoint', 'functor', 'functor', FALSE);
-
 CREATE TABLE structures (
     id TEXT PRIMARY KEY,
     type TEXT NOT NULL,
@@ -39,16 +16,18 @@ CREATE TABLE structures (
     description TEXT NOT NULL,
     nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'),
     dual_structure_id TEXT,
-    parent TEXT,
+    parent_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
-    FOREIGN KEY (parent, type) REFERENCES structures (id, type) ON DELETE RESTRICT
+    FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT,
+    FOREIGN KEY (parent_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 INDEX idx_structures_by_type ON structures (type);
+
+CREATE INDEX idx_structures_by_parent ON structures (parent_structure_id, type);
 
 CREATE TABLE related_structures (
     id INTEGER PRIMARY KEY,
@@ -68,7 +47,7 @@ CREATE TABLE structure_comments (
     FOREIGN KEY (structure_id) REFERENCES structures (id) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_structure_comments ON structure_comments (structure_id);
+CREATE INDEX idx_comments_by_structure ON structure_comments (structure_id);
 
 CREATE TABLE structure_tags (
     id INTEGER PRIMARY KEY,
@@ -87,17 +66,45 @@ CREATE TABLE structure_tag_assignments (
     FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE
 );
 
+CREATE INDEX idx_structures_by_tag ON structure_tag_assignments (type, tag, structure_id);
+
+CREATE TABLE structure_associations (
+    label TEXT NOT NULL,
+    source_type TEXT NOT NULL,
+    target_type TEXT NOT NULL,
+    required INTEGER NOT NULL CHECK (required in (TRUE, FALSE)),
+    PRIMARY KEY (label, source_type),
+    UNIQUE (label, source_type, target_type),
+    FOREIGN KEY (source_type) REFERENCES structure_types (type) ON DELETE CASCADE,
+    FOREIGN KEY (target_type) REFERENCES structure_types (type) ON DELETE CASCADE
+);
+
+INSERT INTO structure_associations
+    (label, source_type, target_type, required)
+VALUES
+    ('domain', 'functor', 'category', TRUE),
+    ('codomain', 'functor', 'category', TRUE),
+    ('category', 'morphism', 'category', TRUE),
+    ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE),
+    ('left_adjoint', 'functor', 'functor', FALSE),
+    ('right_adjoint', 'functor', 'functor', FALSE);
+
 CREATE TABLE associated_structures (
     label TEXT NOT NULL,
-    type TEXT NOT NULL,
-    associated_type TEXT NOT NULL,
-    structure_id TEXT NOT NULL,
-    associated_structure_id TEXT NOT NULL,
-    FOREIGN KEY (label, type, associated_type)
-        REFERENCES associated_structure_types (label, type, associated_type)
+    source_type TEXT NOT NULL,
+    target_type TEXT NOT NULL,
+    source_structure_id TEXT NOT NULL,
+    target_structure_id TEXT NOT NULL,
+    PRIMARY KEY (label, source_type, source_structure_id),
+    FOREIGN KEY (label, source_type, target_type)
+        REFERENCES structure_associations (label, source_type, target_type)
         ON DELETE CASCADE,
-    FOREIGN KEY (structure_id, type)
+    FOREIGN KEY (source_structure_id, source_type)
         REFERENCES structures (id, type) ON DELETE CASCADE,
-    FOREIGN KEY (associated_structure_id, associated_type)
+    FOREIGN KEY (target_structure_id, target_type)
         REFERENCES structures (id, type) ON DELETE CASCADE
-);
+);
+
+CREATE INDEX idx_associated_structures_by_source ON associated_structures (source_structure_id);
+
+CREATE INDEX idx_associated_structures_by_target ON associated_structures (target_structure_id);

database/schema/002_properties.sql

@@ -54,7 +54,7 @@ CREATE TABLE property_assignments (
         REFERENCES properties (id, type) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_property_assigned ON property_assignments (property_id);
+CREATE INDEX idx_property_assignments_by_property ON property_assignments (property_id);
 
 CREATE TABLE property_tags (
     id INTEGER PRIMARY KEY,

database/schema/003_implications.sql

@@ -8,7 +8,7 @@ CREATE TABLE implications (
     dual_implication_id TEXT,
     UNIQUE (id, type),
     FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT,
-    FOREIGN KEY (dual_implication_id) REFERENCES implications (id)
+    FOREIGN KEY (dual_implication_id, type) REFERENCES implications (id, type)
 );
 
 CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id));
@@ -26,7 +26,7 @@ CREATE TABLE assumptions (
         REFERENCES properties (id, type) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_assumptions_property ON assumptions (property_id);
+CREATE INDEX idx_assumptions_by_property ON assumptions (property_id);
 
 CREATE TABLE conclusions (
     implication_id TEXT NOT NULL,
@@ -39,7 +39,7 @@ CREATE TABLE conclusions (
         REFERENCES properties (id, type) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_conclusions_property ON conclusions (property_id);
+CREATE INDEX idx_conclusions_by_property ON conclusions (property_id);
 
 CREATE TABLE associated_assumptions (
     implication_id TEXT NOT NULL,
@@ -53,11 +53,11 @@ CREATE TABLE associated_assumptions (
     FOREIGN KEY (property_id, property_type)
         REFERENCES properties (id, type) ON DELETE CASCADE,
     FOREIGN KEY (label, type, property_type)
-        REFERENCES associated_structure_types (label, type, associated_type)
+        REFERENCES structure_associations (label, source_type, target_type)
         ON DELETE RESTRICT
 );
 
-CREATE INDEX idx_assumptions_associated_property ON associated_assumptions (property_id);
+CREATE INDEX idx_associated_assumptions_by_property ON associated_assumptions (property_id);
 
 CREATE VIEW implications_view AS
     SELECT

database/schema/005_special_objects.sql

@@ -1,18 +1,18 @@
-CREATE TABLE special_object_types (
+CREATE TABLE special_objects (
     id INTEGER PRIMARY KEY,
-    type TEXT NOT NULL UNIQUE,
+    kind TEXT NOT NULL UNIQUE,
     dual TEXT,
-    FOREIGN KEY (dual) REFERENCES special_object_types (type) ON DELETE SET NULL
+    FOREIGN KEY (dual) REFERENCES special_objects (kind) ON DELETE SET NULL
 );
 
 CREATE TABLE special_object_assignments (
     category_id TEXT NOT NULL,
-    type TEXT NOT NULL,
+    kind TEXT NOT NULL,
     description TEXT NOT NULL,
     is_deduced INTEGER NOT NULL DEFAULT FALSE
         CHECK (is_deduced in (TRUE, FALSE)),
-    PRIMARY KEY (category_id, type),
-    FOREIGN KEY (type) REFERENCES special_object_types (type) ON DELETE RESTRICT,
+    PRIMARY KEY (category_id, kind),
+    FOREIGN KEY (kind) REFERENCES special_objects (kind) ON DELETE RESTRICT,
     FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE
 );
 

database/schema/006_special-morphisms.sql

@@ -1,19 +1,19 @@
-CREATE TABLE special_morphism_types (
+CREATE TABLE special_morphisms (
     id INTEGER PRIMARY KEY,
-    type TEXT NOT NULL UNIQUE,
+    kind TEXT NOT NULL UNIQUE,
     dual TEXT,
-    FOREIGN KEY (dual) REFERENCES special_morphism_types (type) ON DELETE SET NULL
+    FOREIGN KEY (dual) REFERENCES special_morphisms (kind) ON DELETE SET NULL
 );
 
 CREATE TABLE special_morphism_assignments (
     category_id TEXT NOT NULL,
-    type TEXT NOT NULL,
+    kind TEXT NOT NULL,
     description TEXT NOT NULL,
     proof TEXT NOT NULL,
     is_deduced INTEGER NOT NULL DEFAULT FALSE
         CHECK (is_deduced in (TRUE, FALSE)),
-    PRIMARY KEY (category_id, type),
-    FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT,
+    PRIMARY KEY (category_id, kind),
+    FOREIGN KEY (kind) REFERENCES special_morphisms (kind) ON DELETE RESTRICT,
     FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE
 );
 
@@ -23,10 +23,10 @@ CREATE TABLE special_morphism_rules (
     id INTEGER PRIMARY KEY,
     property_id TEXT NOT NULL,
     property_type TEXT NOT NULL DEFAULT 'category',
-    type TEXT NOT NULL,
+    kind TEXT NOT NULL,
     description TEXT NOT NULL,
     proof TEXT NOT NULL,
     FOREIGN KEY (property_id, property_type)
         REFERENCES properties (id, type) ON DELETE CASCADE,
-    FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT
+    FOREIGN KEY (kind) REFERENCES special_morphisms (kind) ON DELETE RESTRICT
 );