From 1d78fcec277e6102574cf1717d75fffd9f3fedab Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Mon, 11 May 2026 18:31:42 +0200
Subject: [PATCH 1/3] remove redundant implication

this follows from another one already ("strongly_connected_disjoint_products")
---
 .../catdat/data/category-implications/algebraic.yaml     | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/databases/catdat/data/category-implications/algebraic.yaml b/databases/catdat/data/category-implications/algebraic.yaml
index 759ea038..8b02da58 100644
--- a/databases/catdat/data/category-implications/algebraic.yaml
+++ b/databases/catdat/data/category-implications/algebraic.yaml
@@ -24,15 +24,6 @@
   reason: The regular epimorphisms are precisely the sort-wise surjective homomorphisms, which are clearly stable under pullbacks.
   is_equivalence: false
 
-- id: algebras_with_0_disjoint_products
-  assumptions:
-    - finitary algebraic
-    - pointed
-  conclusions:
-    - disjoint products
-  reason: 'We have a constant in every algebra, let us denoted it by $0$. Then the projection $A \times B \to A$ is clearly surjective, hence an epimorphism. To show that $A \sqcup_{A \times B} B$ is trivial, let $R$ be an algebra which admits homomorphisms $f : A \to R$, $g : B \to R$ such that $f(p_1(a,b)) = g(p_2(a,b))$ for all $(a,b) \times A \times B$. This means $f(a) = g(b)$. In particular, $f(a) = g(0) = 0$. Likewise, $g(b) = 0$, and we are done.'
-  is_equivalence: false
-
 - id: generalized_variety_require_sifted_colimit
   assumptions:
     - generalized variety

From e5d7ffab469617877590f8de43300f0ce70fcff6 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Mon, 11 May 2026 18:33:24 +0200
Subject: [PATCH 2/3] combine trivial consequences for thin categories

---
 databases/catdat/data/category-implications/thin.yaml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/databases/catdat/data/category-implications/thin.yaml b/databases/catdat/data/category-implications/thin.yaml
index 46d0f256..47b161b9 100644
--- a/databases/catdat/data/category-implications/thin.yaml
+++ b/databases/catdat/data/category-implications/thin.yaml
@@ -7,16 +7,9 @@
     - generating set
     - locally essentially small
     - one-way
-  reason: This is trivial. The empty set is generating.
-  is_equivalence: false
-
-- id: thin_consequence
-  assumptions:
-    - thin
-  conclusions:
     - equalizers
     - left cancellative
-  reason: Any two parallel morphisms are equal, so their equalizer is the identity, and every morphism is a monomorphism as well.
+  reason: This is trivial.
   is_equivalence: false
 
 - id: thin_inhabited_consequence

From 0413f186a13bc1ebabfd22fbced7bfadbc7c41bb Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Mon, 11 May 2026 18:42:16 +0200
Subject: [PATCH 3/3] remove unused variables and imports

---
 src/components/Selection.svelte           | 2 +-
 src/routes/category/[id]/+page.svelte     | 2 +-
 src/routes/functor-search/+page.server.ts | 2 +-
 src/routes/lemma/[id]/+page.server.ts     | 2 +-
 src/routes/lemmas/+page.server.ts         | 3 +--
 tsconfig.json                             | 4 +++-
 6 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/components/Selection.svelte b/src/components/Selection.svelte
index 01834f2a..114c816c 100644
--- a/src/components/Selection.svelte
+++ b/src/components/Selection.svelte
@@ -1,7 +1,7 @@
 <script lang="ts">
 	import ChipGroup from './ChipGroup.svelte'
 	import Chip from './Chip.svelte'
-	import { get_comparison_score, normalize_text } from '$lib/client/utils'
+	import { get_comparison_score } from '$lib/client/utils'
 
 	type Props = {
 		title?: string
diff --git a/src/routes/category/[id]/+page.svelte b/src/routes/category/[id]/+page.svelte
index b266c661..07d51f7e 100644
--- a/src/routes/category/[id]/+page.svelte
+++ b/src/routes/category/[id]/+page.svelte
@@ -7,7 +7,7 @@
 	import TextWithReason from '$components/TextWithReason.svelte'
 	import { filter_by_tag, pluralize } from '$lib/client/utils'
 	import CategoryList from '$components/CategoryList.svelte'
-	import { faQuestion, faQuestionCircle } from '@fortawesome/free-solid-svg-icons'
+	import { faQuestion } from '@fortawesome/free-solid-svg-icons'
 	import Fa from 'svelte-fa'
 	import SuggestionForm from '$components/SuggestionForm.svelte'
 
diff --git a/src/routes/functor-search/+page.server.ts b/src/routes/functor-search/+page.server.ts
index 54a2e558..47313e34 100644
--- a/src/routes/functor-search/+page.server.ts
+++ b/src/routes/functor-search/+page.server.ts
@@ -2,7 +2,7 @@ import { query } from '$lib/server/db.catdat'
 import { error } from '@sveltejs/kit'
 import sql from 'sql-template-tag'
 
-export const load = async (event) => {
+export const load = async () => {
 	const { rows, err } = query<{ id: string }>(sql`
 		SELECT id FROM functor_properties ORDER BY lower(id)
 	`)
diff --git a/src/routes/lemma/[id]/+page.server.ts b/src/routes/lemma/[id]/+page.server.ts
index 8d7b2029..2d077771 100644
--- a/src/routes/lemma/[id]/+page.server.ts
+++ b/src/routes/lemma/[id]/+page.server.ts
@@ -1,5 +1,5 @@
 import type { CategoryShort, Lemma } from '$lib/commons/types'
-import { batch, query } from '$lib/server/db.catdat'
+import { batch } from '$lib/server/db.catdat'
 import { render_nested_formulas } from '$lib/server/rendering'
 import { error } from '@sveltejs/kit'
 import sql from 'sql-template-tag'
diff --git a/src/routes/lemmas/+page.server.ts b/src/routes/lemmas/+page.server.ts
index 4ca149d5..92f04457 100644
--- a/src/routes/lemmas/+page.server.ts
+++ b/src/routes/lemmas/+page.server.ts
@@ -1,10 +1,9 @@
 import type { Lemma } from '$lib/commons/types'
 import { query } from '$lib/server/db.catdat'
-import { render_nested_formulas } from '$lib/server/rendering'
 import { error } from '@sveltejs/kit'
 import sql from 'sql-template-tag'
 
-export const load = async (event) => {
+export const load = async () => {
 	const { rows: lemmas, err } = query<Lemma>(
 		sql`SELECT id, title, claim, proof FROM lemmas ORDER BY lower(title)`,
 	)
diff --git a/tsconfig.json b/tsconfig.json
index 0b2d8865..83b331c1 100644
--- a/tsconfig.json
+++ b/tsconfig.json
@@ -9,7 +9,9 @@
 		"skipLibCheck": true,
 		"sourceMap": true,
 		"strict": true,
-		"moduleResolution": "bundler"
+		"moduleResolution": "bundler",
+		"noUnusedLocals": true,
+		"noUnusedParameters": true
 	}
 	// Path aliases are handled by https://svelte.dev/docs/kit/configuration#alias
 	// except $lib which is handled by https://svelte.dev/docs/kit/configuration#files