+
{relation}
{id}
diff --git a/src/components/TextWithReason.svelte b/src/components/TextWithReason.svelte
index 7ca3f4d06..7a8689406 100644
--- a/src/components/TextWithReason.svelte
+++ b/src/components/TextWithReason.svelte
@@ -7,10 +7,9 @@
type Props = {
children: Snippet
reason?: string | null
- heading?: string
}
- let { children, reason, heading = 'Reason' }: Props = $props()
+ let { children, reason }: Props = $props()
const id = $props.id()
@@ -18,7 +17,7 @@
e.stopPropagation()
show_popup({
id,
- heading,
+ heading: 'Reason',
text: reason!,
})
}
diff --git a/src/lib/server/utils.ts b/src/lib/server/utils.ts
index 94318c578..20d4ec3fd 100644
--- a/src/lib/server/utils.ts
+++ b/src/lib/server/utils.ts
@@ -1,7 +1,11 @@
import type {
+ CategoryProperty,
+ CategoryPropertyDB,
FunctorImplicationDB,
FunctorImplicationDisplay,
FunctorProperty,
+ FunctorPropertyAssignment,
+ FunctorPropertyAssignmentDB,
FunctorPropertyDB,
ImplicationDB,
ImplicationDisplay,
@@ -45,6 +49,17 @@ export function display_property(property: PropertyDB): PropertyDisplay {
}
}
+export function display_category_property_assignment(
+ property: CategoryPropertyDB,
+): CategoryProperty {
+ return {
+ id: property.id,
+ reason: property.reason,
+ is_deduced: Boolean(property.is_deduced),
+ relation: property.relation,
+ }
+}
+
export function display_functor_property(property: FunctorPropertyDB): FunctorProperty {
return {
id: property.id,
@@ -56,6 +71,17 @@ export function display_functor_property(property: FunctorPropertyDB): FunctorPr
}
}
+export function display_functor_property_assignment(
+ property: FunctorPropertyAssignmentDB,
+): FunctorPropertyAssignment {
+ return {
+ id: property.id,
+ reason: property.reason,
+ is_deduced: Boolean(property.is_deduced),
+ relation: property.relation,
+ }
+}
+
export function display_functor_implication(
implication: FunctorImplicationDB,
): FunctorImplicationDisplay {
diff --git a/src/routes/category-property/[id]/+page.server.ts b/src/routes/category-property/[id]/+page.server.ts
index 4d06e2246..86942ba12 100644
--- a/src/routes/category-property/[id]/+page.server.ts
+++ b/src/routes/category-property/[id]/+page.server.ts
@@ -15,7 +15,7 @@ export const load = async (event) => {
PropertyDB,
{ id: string },
ImplicationDB,
- CategoryShort & { is_satisfied: 0 | 1 },
+ CategoryShort & { is_satisfied: 0 | 1 | null },
CategoryShort,
]
>([
@@ -95,8 +95,9 @@ export const load = async (event) => {
const related_properties = related.map(({ id }) => id)
- const examples = known_categories.filter((c) => c.is_satisfied)
- const counterexamples = known_categories.filter((c) => !c.is_satisfied)
+ const examples = known_categories.filter((c) => c.is_satisfied === 1)
+ const counterexamples = known_categories.filter((c) => c.is_satisfied === 0)
+ const undecidable_categories = known_categories.filter((c) => c.is_satisfied === null)
const relevant_implications = relevant_implications_db.map(display_implication)
@@ -112,6 +113,7 @@ export const load = async (event) => {
examples,
counterexamples,
unknown_categories,
+ undecidable_categories,
relevant_implications,
})
}
diff --git a/src/routes/category-property/[id]/+page.svelte b/src/routes/category-property/[id]/+page.svelte
index 1362b55c6..8192fb62a 100644
--- a/src/routes/category-property/[id]/+page.svelte
+++ b/src/routes/category-property/[id]/+page.svelte
@@ -107,4 +107,17 @@
+{#if data.undecidable_categories.length}
+ Undecidable categories
+
+
+ {pluralize(data.undecidable_categories.length, {
+ one: 'There is {count} category for which it cannot be decided if this property is satisfied or not.',
+ other: 'There are {count} categories for which it cannot be decided if this property is satisfied or not.',
+ })}
+
+
+
+{/if}
+
diff --git a/src/routes/category/[id]/+page.server.ts b/src/routes/category/[id]/+page.server.ts
index bfe6207e8..e5a7c2e3f 100644
--- a/src/routes/category/[id]/+page.server.ts
+++ b/src/routes/category/[id]/+page.server.ts
@@ -4,7 +4,6 @@ import { batch } from '$lib/server/db.catdat'
import sql from 'sql-template-tag'
import type {
CategoryDisplay,
- CategoryProperty,
CategoryPropertyDB,
CategoryShort,
CommentObject,
@@ -14,6 +13,7 @@ import type {
SpecialObject,
TagObject,
} from '$lib/commons/types'
+import { display_category_property_assignment } from '$lib/server/utils'
export const load = async (event) => {
const id = event.params.id
@@ -23,7 +23,7 @@ export const load = async (event) => {
CategoryDisplay,
RelatedCategory,
TagObject,
- CategoryPropertyDB & { is_satisfied: 0 | 1 },
+ CategoryPropertyDB & { is_satisfied: 0 | 1 | null },
PropertyShort,
SpecialObject,
SpecialMorphism,
@@ -75,8 +75,8 @@ export const load = async (event) => {
cp.reason,
cp.is_deduced,
CASE
- WHEN cp.is_satisfied = TRUE THEN p.relation
- ELSE r.negation
+ WHEN cp.is_satisfied = FALSE THEN r.negation
+ ELSE p.relation
END AS relation
FROM category_property_assignments cp
INNER JOIN category_properties p ON p.id = cp.property_id
@@ -86,13 +86,8 @@ export const load = async (event) => {
`,
// unknown properties
sql`
- SELECT
- p.id,
- p.relation,
- c.comment as reason
+ SELECT p.id, p.relation
FROM category_properties p
- LEFT JOIN category_property_comments c
- ON c.category_id = ${id} AND c.property_id = p.id
WHERE NOT EXISTS (
SELECT 1 FROM category_property_assignments
WHERE category_id = ${id} AND property_id = p.id
@@ -159,23 +154,17 @@ export const load = async (event) => {
const category = categories[0]
const tags = tag_objects.map(({ tag }) => tag)
- const satisfied_properties: CategoryProperty[] = properties_db
- .filter((obj) => obj.is_satisfied)
- .map((p) => ({
- id: p.id,
- reason: p.reason,
- is_deduced: Boolean(p.is_deduced),
- relation: p.relation,
- }))
+ const satisfied_properties = properties_db
+ .filter((obj) => obj.is_satisfied === 1)
+ .map(display_category_property_assignment)
+
+ const unsatisfied_properties = properties_db
+ .filter((obj) => obj.is_satisfied === 0)
+ .map(display_category_property_assignment)
- const unsatisfied_properties: CategoryProperty[] = properties_db
- .filter((obj) => !obj.is_satisfied)
- .map((p) => ({
- id: p.id,
- reason: p.reason,
- is_deduced: Boolean(p.is_deduced),
- relation: p.relation,
- }))
+ const undecidable_properties = properties_db
+ .filter((obj) => obj.is_satisfied === null)
+ .map(display_category_property_assignment)
return render_nested_formulas({
category,
@@ -184,6 +173,7 @@ export const load = async (event) => {
satisfied_properties,
unsatisfied_properties,
unknown_properties,
+ undecidable_properties,
special_objects,
special_morphisms,
undistinguishable_categories,
diff --git a/src/routes/category/[id]/+page.svelte b/src/routes/category/[id]/+page.svelte
index 84f6e4298..958e0b401 100644
--- a/src/routes/category/[id]/+page.svelte
+++ b/src/routes/category/[id]/+page.svelte
@@ -157,13 +157,26 @@
{/if}
-
+
+{#if data.undecidable_properties.length > 0}
+
+ Undecidable properties
+
+ {#if data.undecidable_properties.length > 0}
+
+ {pluralize(data.undecidable_properties.length, {
+ one: 'There is {count} property for which it cannot be decided if it is satisfied or not.',
+ other: 'There are {count} properties for which it cannot be decided if they are satisfied or not.',
+ })}
+
+ {/if}
+
+
+
+{/if}
+
Special objects
diff --git a/src/routes/download/+page.svelte b/src/routes/download/+page.svelte
index 238107ff9..36c9b47ef 100644
--- a/src/routes/download/+page.svelte
+++ b/src/routes/download/+page.svelte
@@ -122,6 +122,12 @@ GROUP BY p.id
ORDER BY undecided_categories DESC LIMIT 10;
+-- Properties which cannot be decided for a given category
+SELECT category_id, property_id, reason
+FROM category_property_assignments
+WHERE is_satisfied IS NULL;
+
+