diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml
index eb8aa8ea..aba24134 100644
--- a/databases/catdat/data/functor-implications/limits preservation.yaml
+++ b/databases/catdat/data/functor-implications/limits preservation.yaml
@@ -194,3 +194,12 @@
- preserves finite coproducts
proof: This is trivial.
is_equivalence: false
+
+- id: regular_functor_definition
+ assumptions:
+ - left exact
+ - preserves regular epimorphisms
+ conclusions:
+ - regular
+ proof: This holds by definition of a regular functor.
+ is_equivalence: true
diff --git a/databases/catdat/data/functor-properties/coregular.yaml b/databases/catdat/data/functor-properties/coregular.yaml
new file mode 100644
index 00000000..8d9a70f5
--- /dev/null
+++ b/databases/catdat/data/functor-properties/coregular.yaml
@@ -0,0 +1,13 @@
+id: coregular
+relation: is
+description: 'A functor $F : \C \to \D$ is coregular when it preserves finite colimits and regular monomorphisms. This notion is used in particular when $\C$ and $\D$ are coregular categories.'
+nlab_link: null
+invariant_under_equivalences: true
+dual_property: regular
+related_properties:
+ - right exact
+ - preserves regular monomorphisms
+
+tags:
+ - colimit preservation
+ - morphism behavior
diff --git a/databases/catdat/data/functor-properties/regular.yaml b/databases/catdat/data/functor-properties/regular.yaml
new file mode 100644
index 00000000..8e0801b1
--- /dev/null
+++ b/databases/catdat/data/functor-properties/regular.yaml
@@ -0,0 +1,13 @@
+id: regular
+relation: is
+description: 'A functor $F : \C \to \D$ is regular when it preserves finite limits and regular epimorphisms. This notion is used in particular when $\C$ and $\D$ are regular categories.'
+nlab_link: https://ncatlab.org/nlab/show/regular+functor
+invariant_under_equivalences: true
+dual_property: coregular
+related_properties:
+ - left exact
+ - preserves regular epimorphisms
+
+tags:
+ - limit preservation
+ - morphism behavior
diff --git a/databases/catdat/schema/002_properties.sql b/databases/catdat/schema/002_properties.sql
index 64e83018..89710619 100644
--- a/databases/catdat/schema/002_properties.sql
+++ b/databases/catdat/schema/002_properties.sql
@@ -4,28 +4,28 @@ CREATE TABLE relations (
);
CREATE TABLE properties (
- id TEXT PRIMARY KEY,
+ id 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,
dual_property_id TEXT,
- UNIQUE (id, type), -- TODO: make (id, type) the primary key
+ PRIMARY KEY (id, type),
FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT,
FOREIGN KEY (dual_property_id, type)
REFERENCES properties (id, type) ON DELETE RESTRICT,
FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT
);
-CREATE UNIQUE INDEX properties_lower_id_unique ON properties (lower(id));
+CREATE UNIQUE INDEX properties_lower_id_unique ON properties (lower(id), type);
CREATE TABLE related_properties (
property_id TEXT NOT NULL,
related_property_id TEXT NOT NULL,
type TEXT NOT NULL,
CHECK (property_id != related_property_id),
- PRIMARY KEY (property_id, related_property_id),
+ PRIMARY KEY (property_id, related_property_id, type),
FOREIGN KEY (property_id, type)
REFERENCES properties (id, type) ON DELETE CASCADE,
FOREIGN KEY (related_property_id, type)
diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts
index c8f8e06d..033d1205 100644
--- a/databases/catdat/scripts/deduce-implications.ts
+++ b/databases/catdat/scripts/deduce-implications.ts
@@ -45,13 +45,15 @@ export function create_dualized_implications(type: StructureType) {
(
SELECT json_group_array(p.dual_property_id)
FROM assumptions a
- LEFT JOIN properties p ON p.id = a.property_id
+ LEFT JOIN properties p
+ ON p.id = a.property_id AND p.type = i.type
WHERE a.implication_id = i.id
) AS dual_assumptions,
(
SELECT json_group_array(p.dual_property_id)
FROM conclusions a
- LEFT JOIN properties p ON p.id = a.property_id
+ LEFT JOIN properties p
+ ON p.id = a.property_id AND p.type = i.type
WHERE a.implication_id = i.id
) AS dual_conclusions,
(
@@ -61,7 +63,8 @@ export function create_dualized_implications(type: StructureType) {
a.map,
json_group_array(p.dual_property_id) AS properties
FROM mapped_assumptions a
- INNER JOIN properties p ON p.id = a.property_id
+ INNER JOIN properties p
+ ON p.id = a.property_id AND p.type = a.property_type
WHERE a.implication_id = i.id
GROUP BY a.map
)
diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json
index bf3952fe..aa0394b2 100644
--- a/databases/catdat/scripts/expected-data/forget_vector.json
+++ b/databases/catdat/scripts/expected-data/forget_vector.json
@@ -42,5 +42,7 @@
"preserves reflexive coequalizers": true,
"preserves coreflexive equalizers": true,
"preserves regular monomorphisms": true,
- "preserves regular epimorphisms": true
+ "preserves regular epimorphisms": true,
+ "regular": true,
+ "coregular": false
}
diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json
index bda5a5f9..cbca186a 100644
--- a/databases/catdat/scripts/expected-data/id_Set.json
+++ b/databases/catdat/scripts/expected-data/id_Set.json
@@ -41,5 +41,7 @@
"dominant": true,
"isomorphism": true,
"preserves regular monomorphisms": true,
- "preserves regular epimorphisms": true
+ "preserves regular epimorphisms": true,
+ "regular": true,
+ "coregular": true
}
diff --git a/databases/catdat/scripts/utils/properties.ts b/databases/catdat/scripts/utils/properties.ts
index b9a1d5b0..68bfc47b 100644
--- a/databases/catdat/scripts/utils/properties.ts
+++ b/databases/catdat/scripts/utils/properties.ts
@@ -24,7 +24,7 @@ export function get_properties_dict(db: Database, type: StructureType) {
r.conditional AS conditional_relation
FROM properties p
INNER JOIN relations r ON r.relation = p.relation
- WHERE type = ?
+ WHERE p.type = ?
ORDER BY lower(p.id)`,
)
.all(type)
diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts
index 80996ed3..3eaaa43d 100644
--- a/src/lib/server/fetchers/missing_data.ts
+++ b/src/lib/server/fetchers/missing_data.ts
@@ -18,13 +18,12 @@ export function fetch_missing_data(type: StructureType) {
sql`
SELECT s.id, s.name, COUNT(*) AS count
FROM structures s
- INNER JOIN properties p
+ INNER JOIN properties p ON p.type = s.type
LEFT JOIN property_assignments pa
ON pa.structure_id = s.id
AND pa.property_id = p.id
WHERE
- p.type = ${type}
- AND s.type = ${type}
+ s.type = ${type}
AND pa.property_id IS NULL
GROUP BY s.id
ORDER BY lower(s.name);
@@ -36,16 +35,13 @@ export function fetch_missing_data(type: StructureType) {
s2.id AS id2, s2.name AS name2
FROM structures s1
JOIN structures s2
- ON s1.id < s2.id
- JOIN properties p
+ ON s1.id < s2.id AND s2.type = s1.type
+ JOIN properties p ON p.type = s1.type
LEFT JOIN property_assignments a1
ON a1.structure_id = s1.id AND a1.property_id = p.id
LEFT JOIN property_assignments a2
ON a2.structure_id = s2.id AND a2.property_id = p.id
- WHERE
- p.type = ${type}
- AND s1.type = ${type}
- AND s2.type = ${type}
+ WHERE s1.type = ${type}
GROUP BY s1.id, s1.name, s2.id, s2.name
HAVING SUM(
CASE
diff --git a/src/lib/server/fetchers/properties.ts b/src/lib/server/fetchers/properties.ts
index 8dbd4ca8..3c90e8da 100644
--- a/src/lib/server/fetchers/properties.ts
+++ b/src/lib/server/fetchers/properties.ts
@@ -83,7 +83,7 @@ export function fetch_tagged_properties(type: StructureType, tag: string) {
SELECT p.id, p.relation
FROM property_tag_assignments t
INNER JOIN properties p
- ON p.id = t.property_id
+ ON p.id = t.property_id AND p.type = ${type}
WHERE t.tag = ${tag} AND t.type = ${type}
ORDER BY lower(id)
`)
diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts
index 5677f693..105c9212 100644
--- a/src/lib/server/fetchers/property.ts
+++ b/src/lib/server/fetchers/property.ts
@@ -31,13 +31,13 @@ export function fetch_property(type: StructureType, id: string) {
nlab_link,
invariant_under_equivalences
FROM properties
- WHERE id = ${id}
+ WHERE id = ${id} AND type = ${type}
`,
// related properties
sql`
SELECT related_property_id AS id
FROM related_properties
- WHERE property_id = ${id}
+ WHERE property_id = ${id} AND type = ${type}
ORDER BY lower(id)
`,
// tags
diff --git a/src/lib/server/fetchers/search.ts b/src/lib/server/fetchers/search.ts
index c363df58..42eb75ee 100644
--- a/src/lib/server/fetchers/search.ts
+++ b/src/lib/server/fetchers/search.ts
@@ -99,7 +99,7 @@ export function fetch_search_results(
SELECT s.id, s.name FROM structures s
INNER JOIN property_assignments a ON a.structure_id = s.id
WHERE
- a.type = ? AND s.type = ?
+ s.type = ? AND a.type = s.type
AND property_id IN (${to_placeholders(all_selected_properties)})
GROUP BY structure_id
HAVING
@@ -128,7 +128,6 @@ export function fetch_search_results(
const { rows: found_structures, err } = query({
sql: search_query,
values: [
- type,
type,
...all_selected_properties,
...satisfied_properties,
diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts
index fbfa1e9b..9929f93c 100644
--- a/src/lib/server/fetchers/structure.ts
+++ b/src/lib/server/fetchers/structure.ts
@@ -68,7 +68,8 @@ export function fetch_structure(type: StructureType, id: string) {
pa.is_deduced,
p.relation
FROM property_assignments pa
- INNER JOIN properties p ON p.id = pa.property_id
+ INNER JOIN properties p
+ ON p.id = pa.property_id AND p.type = pa.type
WHERE pa.structure_id = ${id}
ORDER BY pa.id
`,
@@ -76,7 +77,7 @@ export function fetch_structure(type: StructureType, id: string) {
sql`
SELECT p.id, p.relation
FROM properties p
- WHERE type = ${type} AND NOT EXISTS (
+ WHERE p.type = ${type} AND NOT EXISTS (
SELECT 1 FROM property_assignments
WHERE structure_id = ${id} AND property_id = p.id
)
@@ -86,7 +87,7 @@ export function fetch_structure(type: StructureType, id: string) {
sql`
SELECT u.id, u.name
FROM structures u
- JOIN properties p
+ JOIN properties p ON p.type = u.type
LEFT JOIN property_assignments pa
ON pa.structure_id = ${id}
AND pa.property_id = p.id
@@ -94,8 +95,7 @@ export function fetch_structure(type: StructureType, id: string) {
ON up.structure_id = u.id
AND up.property_id = p.id
WHERE
- p.type = ${type}
- AND u.type = ${type}
+ u.type = ${type}
AND u.id != ${id}
GROUP BY u.id, u.name
HAVING SUM(