From efbb7e8201ed1de7560dc07ad0b8a45453016fc5 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 26 Jun 2026 23:38:33 +0200 Subject: [PATCH 1/4] add "is_deduced" information for special objects / morphisms --- .../catdat/schema/005_special_objects.sql | 2 ++ .../catdat/schema/006_special-morphisms.sql | 2 ++ .../scripts/deduce-special-morphisms.ts | 23 +++++++++++++++---- .../catdat/scripts/deduce-special-objects.ts | 23 +++++++++++++++---- 4 files changed, 40 insertions(+), 10 deletions(-) diff --git a/databases/catdat/schema/005_special_objects.sql b/databases/catdat/schema/005_special_objects.sql index 71aff7b45..0315b6c7d 100644 --- a/databases/catdat/schema/005_special_objects.sql +++ b/databases/catdat/schema/005_special_objects.sql @@ -9,6 +9,8 @@ CREATE TABLE special_objects ( category_id TEXT NOT NULL, type 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, FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE diff --git a/databases/catdat/schema/006_special-morphisms.sql b/databases/catdat/schema/006_special-morphisms.sql index 022e3955b..c5de9b4d8 100644 --- a/databases/catdat/schema/006_special-morphisms.sql +++ b/databases/catdat/schema/006_special-morphisms.sql @@ -10,6 +10,8 @@ CREATE TABLE special_morphisms ( type 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, FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE diff --git a/databases/catdat/scripts/deduce-special-morphisms.ts b/databases/catdat/scripts/deduce-special-morphisms.ts index 957f0cc16..c49b2d064 100644 --- a/databases/catdat/scripts/deduce-special-morphisms.ts +++ b/databases/catdat/scripts/deduce-special-morphisms.ts @@ -8,9 +8,17 @@ const db = get_client() export function deduce_special_morphisms() { console.info('\n--- Deduce special morphisms ---') + clear_deduced_special_morphisms() deduce_special_morphisms_of_dual_categories() } +/** + * Clears deduced special morphisms + */ +function clear_deduced_special_morphisms() { + db.prepare(`DELETE FROM special_morphisms WHERE is_deduced = TRUE`).run() +} + /** * Deduce special morphisms in dual categories. * For example, monomorphisms in C describe epimorphisms in C^op. @@ -18,18 +26,23 @@ 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) + `INSERT INTO special_morphisms ( + category_id, + type, + description, + proof, + is_deduced + ) SELECT c.dual_structure_id, t.dual, m.description, - 'This is deduced from its dual category.' + 'This is deduced from its dual category.', + TRUE 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`, + WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL`, ) .run() diff --git a/databases/catdat/scripts/deduce-special-objects.ts b/databases/catdat/scripts/deduce-special-objects.ts index 5904215cb..c656caf38 100644 --- a/databases/catdat/scripts/deduce-special-objects.ts +++ b/databases/catdat/scripts/deduce-special-objects.ts @@ -4,26 +4,39 @@ const db = get_client() export function deduce_special_objects() { console.info('\n--- Deduce special objects ---') + clear_deduced_special_objects() deduce_special_objects_of_dual_categories() } +/** + * Clears deduced special objects + */ +function clear_deduced_special_objects() { + db.prepare(`DELETE FROM special_objects WHERE is_deduced = TRUE`).run() +} + /** * Deduce special objects in dual categories. * For example, initial objects in C describe the terminal objects in C^op. */ -async function deduce_special_objects_of_dual_categories() { +function deduce_special_objects_of_dual_categories() { const res = db .prepare( - `INSERT INTO special_objects (category_id, type, description) + `INSERT INTO special_objects ( + category_id, + type, + description, + is_deduced + ) SELECT c.dual_structure_id, t.dual, - o.description + o.description, + TRUE 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.type = 'category' AND c.dual_structure_id IS NOT NULL - ON CONFLICT DO NOTHING`, + WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL`, ) .run() From b7253160d13d17f2c8b2836d1f6845e60bf0f845 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 27 Jun 2026 00:00:23 +0200 Subject: [PATCH 2/4] delete deduced properties as a first step this must be done _before_ the properties_dict is generated, otherwise each second deduce run only deduces 0 properties. --- databases/catdat/scripts/deduce-structure-properties.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 12fcc03f2..5dfcc7d03 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -394,14 +394,14 @@ export function deduce_properties_for_structures(type: StructureType) { const db = get_client() + delete_deduced_properties(db, type) + const implications = get_normalized_implications(db, type) const structures = get_structures(db, type) const properties_dict = get_properties_dict(db, type) const get_assigned_properties = get_property_assignments(db, structures, type) const deduction = db.transaction(() => { - delete_deduced_properties(db, type) - for (const structure of structures) { const assigned = get_assigned_properties[structure.id] From 683af62358777f3f29f7c0c165f4583d502239d8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 27 Jun 2026 00:12:56 +0200 Subject: [PATCH 3/4] move restriction of representable functors to the end --- databases/catdat/scripts/deduce.ts | 2 +- databases/catdat/scripts/restrict-functor-properties.ts | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/databases/catdat/scripts/deduce.ts b/databases/catdat/scripts/deduce.ts index b68f7ea04..80c8c69c8 100644 --- a/databases/catdat/scripts/deduce.ts +++ b/databases/catdat/scripts/deduce.ts @@ -23,8 +23,8 @@ function deduce() { deduce_special_morphisms() // --- functors --- - restrict_representable_functors() clear_deduced_implications('functor') create_dualized_implications('functor') deduce_properties_for_structures('functor') + restrict_representable_functors() } diff --git a/databases/catdat/scripts/restrict-functor-properties.ts b/databases/catdat/scripts/restrict-functor-properties.ts index e755fa45c..b2fa8b2af 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -26,7 +26,7 @@ export function restrict_representable_functors() { 'functor', FALSE, 'The target category is not $\\Set$.', - FALSE, + TRUE, FALSE FROM functors f WHERE f.target <> 'Set' From 77b002287f9dc3a8dface377f6585c7d8a34eee3 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 27 Jun 2026 00:21:01 +0200 Subject: [PATCH 4/4] override existing proof to simplify it --- databases/catdat/scripts/restrict-functor-properties.ts | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/databases/catdat/scripts/restrict-functor-properties.ts b/databases/catdat/scripts/restrict-functor-properties.ts index b2fa8b2af..359de3a87 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -30,7 +30,11 @@ export function restrict_representable_functors() { FALSE FROM functors f WHERE f.target <> 'Set' - ON CONFLICT (structure_id, property_id) DO NOTHING`, + ON CONFLICT (structure_id, property_id) + DO UPDATE SET + proof = excluded.proof, + is_deduced = excluded.is_deduced, + check_redundancy = excluded.check_redundancy`, ) .run()