complete revision of schema

Author: ScriptRaccoon

databases/catdat/schema/001_structures.sql

@@ -9,20 +9,50 @@ INSERT INTO structure_types (type) VALUES ('category'), ('functor');
 -- STRUCTURES
 
 CREATE TABLE structures (
-    id TEXT PRIMARY KEY,
+    name TEXT NOT NULL,
     type TEXT NOT NULL,
-    name TEXT NOT NULL UNIQUE,
+    long_name TEXT NOT NULL,
     notation TEXT NOT NULL,
     description TEXT,
     nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'),
-    FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT,
-    UNIQUE (id, type)
+    PRIMARY KEY (name, type),
+    UNIQUE (long_name, type),
+    FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT
 );
 
-CREATE UNIQUE INDEX idx_structures_lower_id_unique ON structures (lower(id));
+CREATE UNIQUE INDEX idx_structures_lower_id_unique ON structures (lower(name), type);
 
 CREATE INDEX idx_structures_by_type ON structures (type);
 
+-- STRUCTURE MAPS
+
+CREATE TABLE structure_maps (
+    name TEXT NOT NULL,
+    input_type TEXT NOT NULL,
+    output_type TEXT NOT NULL,
+    PRIMARY KEY (name, input_type, output_type),
+    FOREIGN KEY (input_type) REFERENCES structure_types (type) ON DELETE RESTRICT,
+    FOREIGN KEY (output_type) REFERENCES structure_types (type) ON DELETE RESTRICT
+);
+
+INSERT INTO structure_maps (name, input_type, output_type) VALUES
+    ('source', 'functor', 'category'),
+    ('target', 'functor', 'category'),
+    ('left_adjoint', 'functor', 'functor');
+
+CREATE TABLE structure_map_values (
+    name TEXT NOT NULL,
+    input TEXT NOT NULL,
+    input_type TEXT NOT NULL,
+    output TEXT NOT NULL,
+    output_type TEXT NOT NULL,
+    PRIMARY KEY (name, input, input_type, output, output_type),
+    FOREIGN KEY (name, input_type, output_type)
+        REFERENCES structure_maps (name, input_type, output_type) ON DELETE CASCADE,
+    FOREIGN KEY (input, input_type) REFERENCES structures (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (output, output_type) REFERENCES structures (name, type) ON DELETE CASCADE
+);
+
 -- TAGS
 
 CREATE TABLE tags (
@@ -36,46 +66,47 @@ CREATE TABLE tags (
 CREATE INDEX idx_tags_by_type ON tags (type);
 
 CREATE TABLE tag_assignments (
-    structure_id TEXT NOT NULL,
+    structure TEXT NOT NULL,
     tag TEXT NOT NULL,
     type TEXT NOT NULL,
-    PRIMARY KEY (structure_id, tag),
-    FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE,
+    PRIMARY KEY (structure, tag),
+    FOREIGN KEY (structure, type) REFERENCES structures (name, type) ON DELETE CASCADE,
     FOREIGN KEY (tag, type) REFERENCES tags (tag, type) ON DELETE CASCADE
 );
 
 -- RELATED AND DUAL STRUCTURES
 
 CREATE TABLE related_structures (
-    structure_id TEXT NOT NULL,
-    related_structure_id TEXT NOT NULL,
-    PRIMARY KEY (structure_id, related_structure_id),
-    FOREIGN KEY (structure_id) REFERENCES structures (id) ON DELETE CASCADE,
-    FOREIGN KEY (related_structure_id) REFERENCES structures (id) ON DELETE CASCADE
-    -- intentionally we do not save the type here
+    structure TEXT NOT NULL,
+    related_structure TEXT NOT NULL,
+    type TEXT NOT NULL,
+    PRIMARY KEY (structure, related_structure, type),
+    FOREIGN KEY (structure, type) REFERENCES structures (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (related_structure, type) REFERENCES structures (name, type) ON DELETE CASCADE
 );
 
 CREATE TABLE dual_structures (
-    structure_id TEXT NOT NULL,
-    dual_structure_id TEXT NOT NULL,
+    structure TEXT NOT NULL,
+    dual_structure TEXT NOT NULL,
     type TEXT NOT NULL,
-    PRIMARY KEY (structure_id, dual_structure_id),
-    FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE,
-    FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE,
-    UNIQUE (structure_id),
-    UNIQUE (dual_structure_id)
+    PRIMARY KEY (structure, dual_structure, type),
+    FOREIGN KEY (structure, type) REFERENCES structures (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (dual_structure, type) REFERENCES structures (name, type) ON DELETE CASCADE,
+    UNIQUE (structure),
+    UNIQUE (dual_structure)
 );
 
 -- COMMENTS
 
 CREATE TABLE structure_comments (
     id INTEGER PRIMARY KEY,
-    structure_id TEXT NOT NULL,
+    structure TEXT NOT NULL,
+    type TEXT NOT NULL,
     comment TEXT NOT NULL,
-    FOREIGN KEY (structure_id) REFERENCES structures (id) ON DELETE CASCADE
+    FOREIGN KEY (structure, type) REFERENCES structures (name, type) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_comments_by_structure ON structure_comments (structure_id);
+CREATE INDEX idx_comments_by_structure ON structure_comments (structure, type);
 
 -- PROPERTIES OF STRUCTURES
 
@@ -85,50 +116,51 @@ CREATE TABLE relations (
 );
 
 CREATE TABLE properties (
-    id TEXT PRIMARY KEY,
+    name TEXT NOT NULL,
     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,
-    UNIQUE (id, type),
+    CHECK (invariant_under_equivalences in (TRUE, FALSE)),
+    PRIMARY KEY (name, type),
     FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT,
     FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT
 );
 
-CREATE UNIQUE INDEX idx_properties_lower_id_unique ON properties (lower(id));
+CREATE UNIQUE INDEX idx_properties_lower_name_unique ON properties (lower(name), type);
 
 CREATE INDEX idx_properties_by_type ON properties (type);
 
 -- RELATED AND DUAL PROPERTIES 
 
 CREATE TABLE related_properties (
-    property_id TEXT NOT NULL,
-    related_property_id TEXT NOT NULL,
-    PRIMARY KEY (property_id, related_property_id),
-    FOREIGN KEY (property_id) REFERENCES properties (id) ON DELETE CASCADE,
-    FOREIGN KEY (related_property_id) REFERENCES properties (id) ON DELETE CASCADE
-    -- intentionally we do not save the type here
+    property TEXT NOT NULL,
+    related_property TEXT NOT NULL,
+    type TEXT NOT NULL,
+    PRIMARY KEY (property, related_property, type),
+    FOREIGN KEY (property, type) REFERENCES properties (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (related_property, type) REFERENCES properties (name, type) ON DELETE CASCADE
 );
 
 CREATE TABLE dual_properties (
-    property_id TEXT NOT NULL,
-    dual_property_id TEXT NOT NULL,
+    property TEXT NOT NULL,
+    dual_property TEXT NOT NULL,
     type TEXT NOT NULL,
-    PRIMARY KEY (property_id, dual_property_id),
-    FOREIGN KEY (property_id, type) REFERENCES properties (id, type) ON DELETE CASCADE,
-    FOREIGN KEY (dual_property_id, type) REFERENCES properties (id, type) ON DELETE CASCADE,
-    UNIQUE (property_id),
-    UNIQUE (dual_property_id)
+    PRIMARY KEY (property, dual_property, type),
+    FOREIGN KEY (property, type) REFERENCES properties (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (dual_property, type) REFERENCES properties (name, type) ON DELETE CASCADE,
+    UNIQUE (property, type),
+    UNIQUE (dual_property, type)
 );
 
 -- PROPERTY ASSIGNMENTS
 
 CREATE TABLE property_assignments (
     id INTEGER PRIMARY KEY,
     type TEXT NOT NULL,
-    structure_id TEXT NOT NULL,
-    property_id TEXT NOT NULL,
+    structure TEXT NOT NULL,
+    property TEXT NOT NULL,
     is_satisfied INTEGER
         -- we use is_satisfied = NULL for undecidable properties
         CHECK (is_satisfied in (TRUE, FALSE, NULL)),
@@ -137,18 +169,18 @@ CREATE TABLE property_assignments (
         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
+    UNIQUE (structure, property, type),
+    FOREIGN KEY (structure, type) REFERENCES structures (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (property, type) REFERENCES properties (name, type) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_assignment_by_property ON property_assignments (property_id);
+CREATE INDEX idx_assignment_by_property ON property_assignments (property, type);
 CREATE INDEX idx_assignment_by_type ON property_assignments (type);
 
 -- IMPLICATIONS BETWEEN PROPERTIES
 
 CREATE TABLE implications (
-    id TEXT PRIMARY KEY,
+    name TEXT NOT NULL,
     type TEXT NOT NULL,
     proof TEXT NOT NULL CHECK (length(proof) > 0),
     is_equivalence INTEGER NOT NULL DEFAULT FALSE
@@ -157,49 +189,44 @@ CREATE TABLE implications (
         CHECK (is_deduced in (TRUE, FALSE)),
     dualized_from TEXT,
     CHECK (dualized_from IS NULL OR is_deduced = TRUE),
-    UNIQUE (id, type),
+    PRIMARY KEY (name, type),
     FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT,
-    FOREIGN KEY (dualized_from, type) REFERENCES implications (id, type) ON DELETE CASCADE
+    FOREIGN KEY (dualized_from, type) REFERENCES implications (name, type) ON DELETE CASCADE
 );
 
-CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id));
+CREATE UNIQUE INDEX idx_implications_lower_name_unique ON implications (lower(name), type);
 
-CREATE TABLE implication_properties (
-    implication_id TEXT NOT NULL,
-    property_id TEXT NOT NULL,
+CREATE TABLE assumptions (
+    implication TEXT NOT NULL,
+    property TEXT NOT NULL,
     type TEXT NOT NULL,
-    kind TEXT NOT NULL
-        CHECK (kind in ('assumption', 'conclusion')),
-    structure TEXT NOT NULL
-        CHECK (structure in ('self', 'source', 'target')),
-    PRIMARY KEY (implication_id, property_id, kind, structure),
-    FOREIGN KEY (implication_id, type) REFERENCES implications (id, type) ON DELETE CASCADE,
-    FOREIGN KEY (property_id) REFERENCES properties (id) ON DELETE CASCADE
-);
-
-CREATE INDEX idx_implication_property ON implication_properties (property_id);
-
-CREATE TRIGGER trg_implication_properties_type_structure_check
-BEFORE INSERT ON implication_properties
-BEGIN
-    SELECT
-        CASE
-            WHEN NEW.type = 'category'
-                 AND NEW.structure != 'self'
-            THEN RAISE(ABORT, 'Category implications must use structure = self')
-
-            WHEN NEW.type = 'category'
-                 AND (SELECT type FROM properties WHERE id = NEW.property_id) != 'category'
-            THEN RAISE(ABORT, 'Category implications require category properties')
-
-            WHEN NEW.type = 'functor'
-                 AND NEW.structure = 'self'
-                 AND (SELECT type FROM properties WHERE id = NEW.property_id) != 'functor'
-            THEN RAISE(ABORT, 'Functor self-structure requires functor properties')
-
-            WHEN NEW.type = 'functor'
-                 AND NEW.structure IN ('source', 'target')
-                 AND (SELECT type FROM properties WHERE id = NEW.property_id) != 'category'
-            THEN RAISE(ABORT, 'Functor source/target require category properties')
-        END;
-END;
+    PRIMARY KEY (implication, property, type),
+    FOREIGN KEY (implication, type) REFERENCES implications (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (property, type) REFERENCES properties (name, type) ON DELETE CASCADE
+);
+
+CREATE TABLE conclusions (
+    implication TEXT NOT NULL,
+    property TEXT NOT NULL,
+    type TEXT NOT NULL,
+    PRIMARY KEY (implication, property, type),
+    FOREIGN KEY (implication, type) REFERENCES implications (name, type) ON DELETE CASCADE,
+    FOREIGN KEY (property, type) REFERENCES properties (name, type) ON DELETE CASCADE
+);
+
+CREATE TABLE mapped_assumptions (
+    name TEXT NOT NULL,
+    implication TEXT NOT NULL,
+    implication_type TEXT NOT NULL,
+    property TEXT NOT NULL,
+    property_type TEXT NOT NULL,
+    FOREIGN KEY (implication, implication_type)
+        REFERENCES implications (name, type)
+        ON DELETE CASCADE,
+    FOREIGN KEY (property, property_type)
+        REFERENCES properties (name, type)
+        ON DELETE CASCADE,
+    FOREIGN KEY (name, implication_type, property_type)
+        REFERENCES structure_maps (name, input_type, output_type)
+        ON DELETE CASCADE
+);

databases/catdat/schema/002_categories.sql

@@ -1,27 +1,18 @@
 CREATE TABLE categories (
-    id TEXT PRIMARY KEY,
+    name TEXT PRIMARY KEY,
+    type NOT NULL DEFAULT 'category' CHECK (type = 'category'),
     objects TEXT NOT NULL,
     morphisms TEXT NOT NULL,
-    FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE
+    FOREIGN KEY (name, type) REFERENCES structures (name, type) ON DELETE CASCADE
 );
 
-CREATE TRIGGER categories_type_check
-BEFORE INSERT ON categories
-FOR EACH ROW
-BEGIN
-    SELECT CASE
-        WHEN (SELECT type FROM structures WHERE id = NEW.id) != 'category'
-        THEN RAISE(ABORT, 'invalid category id')
-    END;
-END;
-
 CREATE VIEW categories_view AS
     SELECT
-        s.id, s.name, s.notation, s.description, s.nlab_link,
-        c.objects, c.morphisms, d.dual_structure_id as dual_category_id
+        s.name, s.name, s.notation, s.description, s.nlab_link,
+        c.objects, c.morphisms, d.dual_structure as dual_category
     FROM categories c
-    INNER JOIN structures s ON s.id = c.id
-    LEFT JOIN dual_structures d on d.structure_id = c.id
+    INNER JOIN structures s ON s.name = c.name
+    LEFT JOIN dual_structures d ON d.structure = c.name AND d.type = c.type
 ;
 
 CREATE TABLE special_object_types (
@@ -32,15 +23,15 @@ CREATE TABLE special_object_types (
 );
 
 CREATE TABLE special_objects (
-    category_id TEXT NOT NULL,
+    category TEXT NOT NULL,
     type TEXT NOT NULL,
     description TEXT NOT NULL,
-    PRIMARY KEY (category_id, type),
+    PRIMARY KEY (category, type),
     FOREIGN KEY (type) REFERENCES special_object_types (type) ON DELETE RESTRICT,
-    FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE
+    FOREIGN KEY (category) REFERENCES categories (name) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_special_objects_by_category ON special_objects (category_id);
+CREATE INDEX idx_special_objects_by_category ON special_objects (category);
 
 CREATE TABLE special_morphism_types (
     id INTEGER PRIMARY KEY,
@@ -50,13 +41,13 @@ CREATE TABLE special_morphism_types (
 );
 
 CREATE TABLE special_morphisms (
-    category_id TEXT NOT NULL,
+    category TEXT NOT NULL,
     type TEXT NOT NULL,
     description TEXT NOT NULL,
     proof TEXT NOT NULL,
-    PRIMARY KEY (category_id, type),
+    PRIMARY KEY (category, type),
     FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT,
-    FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE
+    FOREIGN KEY (category) REFERENCES categories (name) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_special_morphisms_by_category ON special_morphisms (category_id);
+CREATE INDEX idx_special_morphisms_by_category ON special_morphisms (category);