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
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
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