diff --git a/databases/catdat/schema/005_special_objects.sql b/databases/catdat/schema/005_special_objects.sql index 71aff7b4..0315b6c7 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 022e3955..c5de9b4d 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 957f0cc1..c49b2d06 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 5904215c..c656caf3 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() diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 12fcc03f..5dfcc7d0 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] diff --git a/databases/catdat/scripts/deduce.ts b/databases/catdat/scripts/deduce.ts index b68f7ea0..80c8c69c 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 e755fa45..359de3a8 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -26,11 +26,15 @@ export function restrict_representable_functors() { 'functor', FALSE, 'The target category is not $\\Set$.', - FALSE, + TRUE, 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()