add more fields to structures table, remove functors table (WIP)

the fields source, target, left_adjoint are moved to the structures table, which makes the functors table redundant. this might be useful later when adding, say, monoidal functors, where source refers to a monoidal category then. also, it justifies more the existence of the source_assumptions table for general implications.

on the other hand, this yields many NULL columns for categories. I am not sure if I should keep it.

Author: ScriptRaccoon

databases/catdat/schema/001_structures.sql

@@ -13,10 +13,16 @@ CREATE TABLE structures (
     notation TEXT NOT NULL,
     description TEXT,
     nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'),
-    dual_structure_id TEXT,
+    dual_structure_id TEXT, -- e.g. for categories
+    source TEXT, -- e.g. for functors
+    target TEXT, -- e.g. for functors
+    left_adjoint TEXT, -- e.g. for functors
     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 (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT,
+    FOREIGN KEY (source) REFERENCES structures (id),
+    FOREIGN KEY (target) REFERENCES structures (id),
+    FOREIGN KEY (left_adjoint) REFERENCES structures (id)
 );
 
 CREATE UNIQUE INDEX structures_lower_id_unique ON structures (lower(id));
@@ -39,6 +45,4 @@ 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_structure_comments ON structure_comments (structure_id);

databases/catdat/schema/004_categories.sql

@@ -14,4 +14,19 @@ BEGIN
               (SELECT type FROM structures WHERE id = NEW.id) != 'category'
             THEN RAISE(ABORT, 'Categories must have type "category"')
         END;
+END;
+
+CREATE TRIGGER trg_category_insert_check
+BEFORE INSERT ON structures
+WHEN NEW.type = 'category'
+BEGIN
+    SELECT CASE
+        WHEN NEW.source IS NOT NULL
+        THEN RAISE(ABORT, 'Categories cannot have a source')
+    END;
+
+    SELECT CASE
+        WHEN NEW.target IS NOT NULL
+        THEN RAISE(ABORT, 'Categories cannot have a target')
+    END;
 END;

databases/catdat/schema/007_functors.sql

@@ -1,19 +1,34 @@
-CREATE TABLE functors (
-    id TEXT PRIMARY KEY,
-    source TEXT NOT NULL,
-    target TEXT NOT NULL,
-    FOREIGN KEY (source) REFERENCES categories (id) ON DELETE CASCADE,
-    FOREIGN KEY (target) REFERENCES categories (id) ON DELETE CASCADE,
-    FOREIGN KEY (id)  REFERENCES structures (id) ON DELETE CASCADE
-);
-
-CREATE TRIGGER trg_functor_type_check
-BEFORE INSERT ON functors
+CREATE TRIGGER trg_functor_insert_check
+BEFORE INSERT ON structures
+WHEN NEW.type = 'functor'
 BEGIN
-    SELECT
-        CASE
-            WHEN 
-              (SELECT type FROM structures WHERE id = NEW.id) != 'functor'
-            THEN RAISE(ABORT, 'Functors must have type "functor"')
-        END;
-END;
+    SELECT CASE
+        WHEN NEW.source IS NULL
+        THEN RAISE(ABORT, 'Functor source must be defined')
+    END;
+
+    SELECT CASE
+        WHEN NEW.target IS NULL
+        THEN RAISE(ABORT, 'Functor target must be defined')
+    END;
+
+    SELECT CASE
+        WHEN NOT EXISTS (
+            SELECT 1
+            FROM structures
+            WHERE id = NEW.source AND type = 'category'
+        )
+        THEN RAISE(ABORT, 'Functor source must reference an existing category')
+    END;
+
+    SELECT CASE
+        WHEN NOT EXISTS (
+            SELECT 1
+            FROM structures
+            WHERE id = NEW.target AND type = 'category'
+        )
+        THEN RAISE(ABORT, 'Functor target must reference an existing category')
+    END;
+END;
+
+-- TODO: add trigger that checks that adjoint functors behave as expected

databases/catdat/schema/008_adjoint-functors.sql

@@ -37,32 +37,34 @@ CREATE TABLE conclusions (
         REFERENCES properties (id, type) ON DELETE CASCADE
 );
 
--- property of source category of a functor (can be generalized when required)
+-- property of the source structure (e.g. of a functor)
 CREATE TABLE source_assumptions (
     implication_id TEXT NOT NULL,
     property_id TEXT NOT NULL,
-    type TEXT NOT NULL CHECK (type = 'functor'),
-    property_type TEXT NOT NULL CHECK (property_type = 'category'),
+    type TEXT NOT NULL,
+    property_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, property_type)
         REFERENCES properties (id, type) ON DELETE CASCADE
 );
 
--- property of target category of a functor (can be generalized when required)
+-- properties of the target structure (e.g. of a functor)
 CREATE TABLE target_assumptions (
     implication_id TEXT NOT NULL,
     property_id TEXT NOT NULL,
-    type TEXT NOT NULL CHECK (type = 'functor'),
-    property_type TEXT NOT NULL CHECK (property_type = 'category'),
+    type TEXT NOT NULL,
+    property_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, property_type)
         REFERENCES properties (id, type) ON DELETE CASCADE
 );
 
+--  TODO: add left_adjoint_assumptions and right_adjoint_assumptions tables
+
 CREATE INDEX idx_assumptions_property ON assumptions (property_id);
 
 CREATE INDEX idx_conclusions_property ON conclusions (property_id);

…bases/catdat/schema/009_implications.sql …bases/catdat/schema/008_implications.sqldatabases/catdat/schema/009_implications.sql renamed to databases/catdat/schema/008_implications.sql databases/catdat/schema/009_implications.sql renamed to databases/catdat/schema/008_implications.sql

@@ -21,15 +21,15 @@ export function restrict_representable_functors() {
                 check_redundancy
             )
             SELECT
-                f.id,
+                s.id,
                 'representable',
                 'functor',
                 FALSE,
                 'The target category is not $\\Set$.',
                 FALSE,
                 FALSE
-            FROM functors f
-            WHERE f.target <> 'Set'
+            FROM structures s
+            WHERE s.type = 'functor' AND s.target <> 'Set'
             ON CONFLICT (structure_id, property_id) DO NOTHING`,
 		)
 		.run()

databases/catdat/scripts/restrict-functor-properties.ts

@@ -4,7 +4,6 @@ import type {
 	CategoryYaml,
 	ConfigYaml,
 	ImplicationYaml,
-	FunctorYaml,
 	PropertyEntry,
 	StructureYaml,
 	PropertyYaml,
@@ -34,7 +33,7 @@ function seed() {
 
 	seed_properties({ type: 'functor', folder: 'functor-properties' })
 	seed_implications({ type: 'functor', folder: 'functor-implications' })
-	seed_structures({ type: 'functor', folder: 'functors', extra: insert_functor })
+	seed_structures({ type: 'functor', folder: 'functors' })
 }
 
 /**
@@ -68,7 +67,6 @@ function clear_all_tables() {
 
 		db.prepare(`DELETE FROM source_assumptions`).run()
 		db.prepare(`DELETE FROM target_assumptions`).run()
-		db.prepare(`DELETE FROM adjoint_functors`).run()
 
 		db.prepare(`DELETE FROM assumptions`).run()
 		db.prepare(`DELETE FROM conclusions`).run()
@@ -162,9 +160,9 @@ function seed_structures<T extends StructureYaml>({
 	const structure_insert = db.prepare(
 		`INSERT INTO structures (
 			id, type, name, notation, description, nlab_link,
-			dual_structure_id
+			dual_structure_id, source, target, left_adjoint
 		)
-		VALUES (?, ?, ?, ?, ?, ?, ?)`,
+		VALUES (?, ?, ?, ?, ?, ?, ?, ?, ?, ?)`,
 	)
 
 	const tag_insert = db.prepare(
@@ -214,6 +212,9 @@ function seed_structures<T extends StructureYaml>({
 			structure.description,
 			structure.nlab_link,
 			structure[`dual_${type}`] || null,
+			structure.source || null,
+			structure.target || null,
+			structure.left_adjoint || null,
 		)
 
 		for (const tag of structure.tags) {
@@ -274,27 +275,6 @@ function insert_category(category: CategoryYaml) {
 	}
 }
 
-/**
- * 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) VALUES (?, ?, ?)`,
-	)
-
-	const adjoint_insert = db.prepare(
-		`INSERT INTO adjoint_functors (left_adjoint, right_adjoint)
-		VALUES (?, ?)
-		ON CONFLICT (left_adjoint, right_adjoint) DO NOTHING`,
-	)
-
-	functor_insert.run(functor.id, functor.source, functor.target)
-
-	if (functor.left_adjoint) {
-		adjoint_insert.run(functor.left_adjoint, functor.id)
-	}
-}
-
 /**
  * Seeds all properties of a given type from YAML files.
  */

databases/catdat/scripts/seed.ts

@@ -37,12 +37,14 @@ export type StructureYaml = {
 	notation: string
 	description?: string | null
 	nlab_link?: string
-	left_adjoint?: string
 	tags: string[]
+	source?: string
+	target?: string
+	left_adjoint?: string
 	related_categories?: string[] // TODO: improve this
 	related_functors?: string[]
 	dual_category?: string // TODO: improve this
-	dual_functor?: string
+	dual_functor?: string // TODO: improve this
 	satisfied_properties: PropertyEntry[]
 	unsatisfied_properties: PropertyEntry[]
 	undecidable_properties?: PropertyEntry[]
@@ -52,17 +54,10 @@ export type StructureYaml = {
 export type CategoryYaml = StructureYaml & {
 	objects: string
 	morphisms: string
-	dual_category?: string | null
 	special_objects: Record<string, ObjectEntry | undefined>
 	special_morphisms: Record<string, MorphismEntry | undefined>
 }
 
-export type FunctorYaml = StructureYaml & {
-	source: string
-	target: string
-	left_adjoint?: string
-}
-
 export type PropertyYaml = {
 	id: string
 	relation: string

databases/catdat/scripts/seed.types.ts

@@ -28,17 +28,17 @@ export function get_functors(db: Database): FunctorMeta[] {
 			}
 		>(
 			`SELECT
-				f.id,
+				s.id,
 				s.name,
-				f.source,
-				f.target,
+				s.source,
+				s.target,
 				(
 					SELECT json_group_array(property_id) FROM (
 						SELECT property_id
 						FROM property_assignments
 						WHERE
 							type = 'category'
-							AND structure_id = f.source
+							AND structure_id = s.source
 							AND is_satisfied = TRUE
 					)
 				) AS source_props,
@@ -48,12 +48,12 @@ export function get_functors(db: Database): FunctorMeta[] {
 						FROM property_assignments
 						WHERE
 							type = 'category'
-							AND structure_id = f.target
+							AND structure_id = s.target
 							AND is_satisfied = TRUE
 					)
 				) AS target_props
-			FROM functors f
-			INNER JOIN structures s ON s.id = f.id
+			FROM structures s
+			WHERE s.type = 'functor'
 			ORDER BY lower(s.name)`,
 		)
 		.all()

databases/catdat/scripts/utils/functors.ts

@@ -31,11 +31,17 @@ export type CategorySpecificDisplay = {
 
 export type FunctorSpecificDisplay = {
 	source: string
-	target: string
 	source_name: string
-	target_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 TagObject = { tag: string }