Add link to dual implication on implication page

DATABASE.md

@@ -103,6 +103,6 @@ to check for redundant assignments of properties to categorical structures.
 
 ## Diagram
 
-This is the database schema as of 15.08.2026; changes may occur.
+This is the database schema as of 18.09.2026; changes may occur.
 
-<img alt="database diagram" src="https://github.com/user-attachments/assets/a2cb788e-cac0-44c6-80fc-ae07de2fe83a" />
+<img alt="database diagram" src="https://github.com/user-attachments/assets/31a8e7f3-59b0-4d57-8d06-0aa554e8159a" />

database/schema/003_implications.sql

@@ -5,8 +5,10 @@ CREATE TABLE implications (
     is_equivalence INTEGER NOT NULL DEFAULT FALSE
         CHECK (is_equivalence IN (TRUE, FALSE)),
     is_deduced INTEGER NOT NULL DEFAULT FALSE,
+    dual_implication_id TEXT,
     UNIQUE (id, type),
-    FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT
+    FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT,
+    FOREIGN KEY (dual_implication_id) REFERENCES implications (id)
 );
 
 CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id));
@@ -64,6 +66,7 @@ CREATE VIEW implications_view AS
         i.is_equivalence,
         i.is_deduced,
         i.proof,
+        i.dual_implication_id,
         (
             SELECT json_group_array(a.property_id)
             FROM assumptions a WHERE a.implication_id = i.id

database/scripts/deduce-implications.ts

@@ -83,8 +83,12 @@ export function create_dualized_implications(type: StructureType) {
 
 	const implication_insert = db.prepare(`
 		INSERT INTO implications
-			(id, type, is_equivalence, proof, is_deduced)
-		VALUES (?, ?, ?, ?, TRUE)	
+			(id, type, is_equivalence, proof, is_deduced, dual_implication_id)
+		VALUES (?, ?, ?, ?, TRUE, ?)	
+	`)
+
+	const dual_update = db.prepare(`
+		UPDATE implications SET dual_implication_id = ? WHERE id = ?	
 	`)
 
 	const assumption_insert = db.prepare(`
@@ -139,9 +143,12 @@ export function create_dualized_implications(type: StructureType) {
 				dual_id,
 				type,
 				impl.is_equivalence,
-				`This follows from the <a href="/${type}-implication/${impl.id}">dual implication</a>.`
+				`This follows from the <a href="/${type}-implication/${impl.id}">dual implication</a>.`,
+				impl.id
 			)
 
+			dual_update.run(dual_id, impl.id)
+
 			for (const a of dual_assumptions) {
 				assumption_insert.run(dual_id, a, type)
 			}

src/lib/commons/types.ts

@@ -94,6 +94,7 @@ export type ImplicationDB = {
 	is_equivalence: 0 | 1
 	is_deduced: 0 | 1
 	proof: string
+	dual_implication_id?: string | null
 	assumptions: string
 	conclusions: string
 	associated_assumptions: string

src/lib/server/fetchers/implication.ts

@@ -19,6 +19,7 @@ export function fetch_implication(type: StructureType, id: string) {
                 is_equivalence,
                 is_deduced,
                 proof,
+				dual_implication_id,
                 assumptions,
                 conclusions,
                 associated_assumptions

src/lib/server/transforms.ts

@@ -37,6 +37,7 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp
 		is_equivalence: Boolean(implication.is_equivalence),
 		is_deduced: Boolean(implication.is_deduced),
 		proof: implication.proof,
+		dual_implication_id: implication.dual_implication_id,
 		assumptions: JSON.parse(implication.assumptions),
 		conclusions: JSON.parse(implication.conclusions),
 		associated_assumptions: parse_nested_json_set(implication.associated_assumptions)

src/pages/ImplicationPage.svelte

@@ -12,7 +12,7 @@
 	} from '$lib/commons/types'
 	import { PLURALS } from '$shared/config'
 	import Fa from 'svelte-fa'
-	import { faCircleArrowLeft } from '@fortawesome/free-solid-svg-icons'
+	import { faCircleArrowLeft, faInfoCircle } from '@fortawesome/free-solid-svg-icons'
 
 	type Props = {
 		type: StructureType
@@ -101,6 +101,14 @@
 	{@html implication.proof}
 </p>
 
+{#if implication.dual_implication_id}
+	<p>
+		<Fa icon={faInfoCircle} />
+		This implication has a
+		<a href="/{type}-implication/{implication.dual_implication_id}">dual</a>.
+	</p>
+{/if}
+
 {#if structures.length > 0}
 	<details>
 		<summary class="hint">

tests/category-implications.spec.ts

@@ -48,6 +48,10 @@ test('user can see the details of an implication', async ({ page }) => {
 		})
 	).toBeVisible()
 
+	await expect(page.locator('body')).toContainText(
+		'If a category is cartesian closed, then it has finite products.'
+	)
+
 	await expect(
 		page.getByRole('link', {
 			name: 'cartesian closed',
@@ -65,6 +69,22 @@ test('user can see the details of an implication', async ({ page }) => {
 	await expect(page.locator('body')).toContainText('Proof: This holds by definition')
 })
 
+test('user can navigate to the dual implication', async ({ page }) => {
+	await page.goto('/category-implication/abelian_implies_regular')
+
+	await expect(page.locator('body')).toContainText(
+		'If a category is abelian, then it is regular.'
+	)
+
+	await page.getByRole('link', { name: 'dual' }).click()
+
+	await expect(page).toHaveURL('/category-implication/dual_abelian_implies_regular')
+
+	await expect(page.locator('body')).toContainText(
+		'If a category is abelian, then it is coregular.'
+	)
+})
+
 test('user can open the list of deduced implications', async ({ page }) => {
 	await page.goto('/category-implications', { waitUntil: 'networkidle' })
 

tests/functor-implications.spec.ts

@@ -48,6 +48,10 @@ test('user can see the details of an implication', async ({ page }) => {
 		})
 	).toBeVisible()
 
+	await expect(page.locator('body')).toContainText(
+		'If a functor is fully faithful, then it is conservative.'
+	)
+
 	await expect(
 		page.getByRole('link', {
 			name: 'fully faithful',
@@ -65,6 +69,22 @@ test('user can see the details of an implication', async ({ page }) => {
 	await expect(page.locator('body')).toContainText(/Proof:.+follows that/)
 })
 
+test('user can navigate to the dual implication', async ({ page }) => {
+	await page.goto('/functor-implication/equivalence_consequences')
+
+	await expect(page.locator('body')).toContainText(
+		'If a functor is an equivalence, then it is monadic and is a reflector.'
+	)
+
+	await page.getByRole('link', { name: 'dual' }).click()
+
+	await expect(page).toHaveURL('/functor-implication/dual_equivalence_consequences')
+
+	await expect(page.locator('body')).toContainText(
+		'If a functor is an equivalence, then it is comonadic and is a coreflector.'
+	)
+})
+
 test('user can open the list of deduced implications', async ({ page }) => {
 	await page.goto('/functor-implications', { waitUntil: 'networkidle' })
 

tests/morphism-implications.spec.ts

@@ -50,6 +50,10 @@ test('user can see the details of an implication', async ({ page }) => {
 		})
 	).toBeVisible()
 
+	await expect(page.locator('body')).toContainText(
+		'If a morphism is a split monomorphism, then it is a regular monomorphism.'
+	)
+
 	await expect(
 		page.getByRole('link', {
 			name: 'split monomorphism',
@@ -67,6 +71,22 @@ test('user can see the details of an implication', async ({ page }) => {
 	await expect(page.locator('body')).toContainText('Proof: Let')
 })
 
+test('user can navigate to the dual implication', async ({ page }) => {
+	await page.goto('/morphism-implication/split_mono_epi_is_iso')
+
+	await expect(page.locator('body')).toContainText(
+		'If a morphism is an epimorphism and is a split monomorphism, then it is an isomorphism.'
+	)
+
+	await page.getByRole('link', { name: 'dual' }).click()
+
+	await expect(page).toHaveURL('/morphism-implication/dual_split_mono_epi_is_iso')
+
+	await expect(page.locator('body')).toContainText(
+		'If a morphism is a monomorphism and is a split epimorphism, then it is an isomorphism.'
+	)
+})
+
 test('user can open the list of deduced implications', async ({ page }) => {
 	await page.goto('/morphism-implications', { waitUntil: 'networkidle' })