Show implication usage

databases/catdat/data/category-implications/initial objects.yaml

@@ -34,12 +34,3 @@
     - strict initial object
   reason: 'It suffices to prove that in general any monomorphism $f : A \to 0$ into an initial object is an isomorphism. If $g : 0 \to A$ is the unique morphism, then $f \circ g = \id_0$ since $0$ is initial. But then $f$ is a split epimorphism and a monomorphism, hence an isomorphism.'
   is_equivalence: false
-
-- id: strict_initial_right_criterion
-  assumptions:
-    - initial object
-    - right cancellative
-  conclusions:
-    - strict initial object
-  reason: 'Let $f : A \to 0$ be a morphism. Let $g : 0 \to A$ be the unique morphism. It is an epimorphism by assumption. Also, $f \circ g = \id_0$ since $0$ is initial. But then $g$ is a split monomorphism and an epimorphism, hence an isomorphism.'
-  is_equivalence: false

src/routes/app.css

@@ -111,6 +111,10 @@ p {
 	margin-block: 1rem;
 }
 
+details {
+	margin-block: 1rem;
+}
+
 a {
 	color: inherit;
 	text-underline-offset: 2px;

src/routes/category-implication/[id]/+page.server.ts

@@ -1,5 +1,5 @@
-import type { ImplicationDB, ImplicationDisplay } from '$lib/commons/types'
-import { query } from '$lib/server/db.catdat'
+import type { CategoryShort, ImplicationDB, ImplicationDisplay } from '$lib/commons/types'
+import { batch } from '$lib/server/db.catdat'
 import { render_nested_formulas } from '$lib/server/formulas'
 import { display_implication } from '$lib/server/utils'
 import { error } from '@sveltejs/kit'
@@ -8,24 +8,36 @@ import sql from 'sql-template-tag'
 export const load = async (event) => {
 	const id = event.params.id
 
-	const { rows, err } = query<ImplicationDB>(sql`
-		SELECT
-			id,
-			is_equivalence,
-			reason,
-			assumptions,
-			conclusions,
-			is_deduced,
-            dualized_from
-		FROM category_implications_view
-        WHERE id = ${id}
-	`)
+	const { results, err } = batch<[ImplicationDB, CategoryShort]>([
+		sql`
+			SELECT
+				id,
+				is_equivalence,
+				reason,
+				assumptions,
+				conclusions,
+				is_deduced,
+				dualized_from
+			FROM category_implications_view
+			WHERE id = ${id}
+		`,
+		sql`
+			SELECT c.id, c.name FROM categories c
+			WHERE EXISTS (
+				SELECT 1 FROM category_property_assignments cp
+				WHERE cp.category_id = c.id
+				AND cp.reason LIKE '%/category-implication/' || ${id} || '%'
+			)
+		`,
+	])
 
 	if (err) error(500, 'Could not load implication')
 
-	if (!rows.length) error(404, `Could not find implication with ID '${id}'`)
+	const [implications, categories] = results
 
-	const implication: ImplicationDisplay = display_implication(rows[0])
+	if (!implications.length) error(404, `Could not find implication with ID '${id}'`)
 
-	return render_nested_formulas({ implication })
+	const implication: ImplicationDisplay = display_implication(implications[0])
+
+	return render_nested_formulas({ implication, categories })
 }

src/routes/category-implication/[id]/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
+	import CategoryList from '$components/CategoryList.svelte'
 	import MetaData from '$components/MetaData.svelte'
 	import SuggestionForm from '$components/SuggestionForm.svelte'
+	import { pluralize } from '$lib/client/utils'
 	import { get_property_url } from '$lib/commons/property.url'
 	import { faInfoCircle } from '@fortawesome/free-solid-svg-icons'
 	import Fa from 'svelte-fa'
@@ -55,6 +57,18 @@
 	</p>
 {/if}
 
+{#if data.categories.length > 0}
+	<details>
+		<summary class="hint">
+			{pluralize(data.categories.length, {
+				one: 'Show {count} category using this implication',
+				other: 'Show {count} categories using this implication',
+			})}
+		</summary>
+		<CategoryList categories={data.categories} />
+	</details>
+{/if}
+
 <button class="button" onclick={() => window.history.back()}>Go back</button>
 
 <SuggestionForm />

src/routes/functor-implication/[id]/+page.server.ts

@@ -1,34 +1,52 @@
 import { render_nested_formulas } from '$lib/server/formulas'
-import { query } from '$lib/server/db.catdat'
+import { batch } from '$lib/server/db.catdat'
 import sql from 'sql-template-tag'
 import { error } from '@sveltejs/kit'
-import type { FunctorImplicationDB, FunctorImplicationDisplay } from '$lib/commons/types'
+import type {
+	FunctorImplicationDB,
+	FunctorImplicationDisplay,
+	FunctorShort,
+} from '$lib/commons/types'
 import { display_functor_implication } from '$lib/server/utils'
 
 export const prerender = true
 
 export const load = async (event) => {
 	const id = event.params.id
 
-	const { rows, err } = query<FunctorImplicationDB>(sql`
-        SELECT
-            id,
-            is_equivalence,
-            reason,
-            assumptions,
-            conclusions,
-            source_assumptions,
-            target_assumptions,
-			dualized_from
-        FROM functor_implications_view
-        WHERE id = ${id}
-    `)
+	const { results, err } = batch<[FunctorImplicationDB, FunctorShort]>([
+		sql`
+            SELECT
+                id,
+                is_equivalence,
+                reason,
+                assumptions,
+                conclusions,
+                source_assumptions,
+                target_assumptions,
+                dualized_from
+            FROM functor_implications_view
+            WHERE id = ${id}
+        `,
+		sql`
+            SELECT f.id, f.name FROM functors f
+            WHERE EXISTS (
+                SELECT 1 FROM functor_property_assignments fp
+                WHERE fp.functor_id = f.id
+                AND fp.reason LIKE '%/functor-implication/' || ${id} || '%'
+            )
+        `,
+	])
 
 	if (err) error(500, 'Could not load implication')
 
-	if (!rows.length) error(404, `Could not find implication with ID '${id}'`)
+	const [implications, functors] = results
 
-	const implication: FunctorImplicationDisplay = display_functor_implication(rows[0])
+	if (!implications.length) error(404, `Could not find implication with ID '${id}'`)
 
-	return render_nested_formulas({ implication })
+	const implication: FunctorImplicationDisplay = display_functor_implication(
+		implications[0],
+	)
+
+	return render_nested_formulas({ implication, functors })
 }

src/routes/functor-implication/[id]/+page.svelte

@@ -1,6 +1,8 @@
 <script lang="ts">
+	import FunctorList from '$components/FunctorList.svelte'
 	import MetaData from '$components/MetaData.svelte'
 	import SuggestionForm from '$components/SuggestionForm.svelte'
+	import { pluralize } from '$lib/client/utils'
 	import { get_property_url } from '$lib/commons/property.url'
 	import { faInfoCircle } from '@fortawesome/free-solid-svg-icons'
 	import Fa from 'svelte-fa'
@@ -81,6 +83,18 @@
 	</p>
 {/if}
 
+{#if data.functors.length > 0}
+	<details>
+		<summary class="hint">
+			{pluralize(data.functors.length, {
+				one: 'Show {count} functor using this implication',
+				other: 'Show {count} functors using this implication',
+			})}
+		</summary>
+		<FunctorList functors={data.functors} />
+	</details>
+{/if}
+
 <button class="button" onclick={() => window.history.back()}>Go back</button>
 
 <SuggestionForm />