ScriptRaccoon · ScriptRaccoon · Apr 17, 2026 · Apr 16, 2026 · Apr 17, 2026 · Apr 16, 2026
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -17,7 +17,8 @@
 		"Prost",
 		"SetxSet",
 		"hilberts",
-		"maxage"
+		"maxage",
+		"ndash"
 	],
 	"cSpell.words": [
 		"abelian",
@@ -39,6 +40,7 @@
 		"catdat",
 		"clopen",
 		"Clowder",
+		"coaccessible",
 		"cocartesian",
 		"coclosed",
 		"cocomplete",
@@ -70,6 +72,7 @@
 		"conormal",
 		"copower",
 		"copowers",
+		"copresentable",
 		"coprime",
 		"coproduct",
 		"coproducts",
@@ -88,10 +91,12 @@
 		"delooping",
 		"deloopings",
 		"Demazure",
+		"Diers",
 		"diffeomorphism",
 		"diffeomorphisms",
 		"dualizable",
 		"Dualization",
+		"Eilenberg",
 		"endofunctors",
 		"Engelking",
 		"epimorphic",
@@ -130,9 +135,10 @@
 		"Kashiwara",
 		"katex",
 		"Kolmogorov",
-		"lextensive",
+		"Lawvere",
 		"libsql",
 		"Lindelöf",
+		"Makkai",
 		"Malcev",
 		"Mathoverflow",
 		"metrizable",
@@ -148,13 +154,15 @@
 		"Niefield",
 		"nilradical",
 		"nlab",
+		"Noetherian",
 		"objectwise",
 		"pointwise",
 		"Pontryagin",
 		"poset",
 		"posets",
 		"preadditive",
 		"precomposed",
+		"precomposition",
 		"preimage",
 		"preimages",
 		"preordered",

diff --git a/database/data/001_categories/007_tiny.sql b/database/data/001_categories/007_tiny.sql
@@ -12,10 +12,10 @@ VALUES
 (
 	'0',
 	'empty category',
-	'$0$',
+	'$\mathbf{0}$',
 	'no objects',
 	'no morphisms',
-	'This is the category with no objects and no morphisms. It is the initial object in the category of (small) categories.',
+	'This is the category with no objects and no morphisms. It is the initial object in the category of small categories.',
 	'https://ncatlab.org/nlab/show/empty+category',
 	NULL
 ),
@@ -25,17 +25,17 @@ VALUES
 	'$\mathbf{1}$',
 	'a single object $0$',
 	'only the identity morphism',
-	'This is the simplest category, consisting of a single object $0$ and its identity morphism $0 \to 0$. It is the terminal object in the category of small categories.',
+	'This is the simplest category, consisting of a single object $0$ and its identity morphism $0 \to 0$. A concrete representation is the full subcategory of $\mathbf{Set}$ consisting of the empty set. It is the terminal object in the category of small categories.',
 	'https://ncatlab.org/nlab/show/terminal+category',
 	NULL
 ),
 (
 	'2',
 	'discrete category on two objects',
 	'$\mathbf{2}$',
-	'two objects',
+	'two objects $0$ and $1$',
 	'only the two identity morphisms',
-	'For a more concrete representation, this is the subcategory of $\mathbf{CRing}$ of the two fields $\mathbb{F}_2$ and $\mathbb{F}_3$.',
+	'A concrete representation is the full subcategory of $\mathbf{CRing}$ consisting of the two fields $\mathbb{F}_2$ and $\mathbb{F}_3$.',
 	NULL,
 	NULL
 ),

diff --git a/database/data/001_categories/100_related-categories.sql b/database/data/001_categories/100_related-categories.sql
@@ -1,5 +1,7 @@
 INSERT INTO related_categories (category_id, related_category_id)
 VALUES
+('0', '1'),
+('1', '0'),
 ('1', '2'),
 ('2', '1'),
 ('Ab', 'CMon'),

diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql
@@ -164,14 +164,6 @@ VALUES
 	'extensive',
 	TRUE
 ),
-(
-	'lextensive',
-	'is',
-	'A category $\mathcal{C}$ is <i>lextensive</i> when it is extensive and has finite limits.',
-	'https://ncatlab.org/nlab/show/extensive+category',
-	NULL,
-	TRUE
-),
 (
 	'infinitary extensive',
 	'is',

diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql
@@ -217,9 +217,6 @@ VALUES
 ('extensive', 'infinitary extensive'),
 ('extensive', 'finite coproducts'),
 ('extensive', 'disjoint finite coproducts'),
-('extensive', 'lextensive'),
-('lextensive', 'extensive'),
-('lextensive', 'finitely complete'),
 ('infinitary extensive', 'extensive'),
 ('infinitary extensive', 'coproducts'),
 ('infinitary extensive', 'disjoint coproducts'),

diff --git a/database/data/004_property-assignments/Met_c.sql b/database/data/004_property-assignments/Met_c.sql
@@ -97,7 +97,7 @@ VALUES
 ),
 (
 	'Met_c',
-	'coequalizers',
+	'sequential colimits',
 	FALSE,
-	'See <a href="https://mathoverflow.net/a/509582/2841" target="_blank">MO/509548</a>.'
+	'See <a href="https://mathoverflow.net/questions/510316" target="_blank">MO/510316</a>.'
 );
diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql
@@ -49,9 +49,9 @@ VALUES
 	FALSE
 ),
 (
-	'products_consequence',
+	'products_consequences',
 	'["products"]',
-	'["finite products", "countable products"]',
+	'["finite products", "countable products", "powers"]',
 	'This is trivial.',
 	FALSE
 ),
@@ -76,24 +76,10 @@ VALUES
 	'If $1$ is a terminal object, then $X \times_1 Y = X \times Y$.',
 	FALSE
 ),
-(
-	'terminal_consequence',
-	'["terminal object"]',
-	'["connected"]',
-	'If $1$ denotes the terminal object, then for any two objects $A,B$ we have the zig-zag $A \rightarrow 1 \leftarrow B$.',
-	FALSE
-),
-(
-	'binary_products_consequence',
-	'["binary products", "inhabited"]',
-	'["connected"]',
-	'For any two objects $A,B$ we have the zig-zag $A \leftarrow A \times B \rightarrow B$.',
-	FALSE
-),
 (
 	'countable_products_consequence',
 	'["countable products"]',
-	'["finite products"]',
+	'["finite products", "countable powers"]',
 	'This is trivial.',
 	FALSE
 ),
@@ -206,7 +192,7 @@ VALUES
 	'wide_pullbacks_finite',
 	'["pullbacks", "essentially finite"]',
 	'["wide pullbacks"]',
-	'Each slice category has finite products and is essentially finite, <a href="/category-implication/freyd_finite">hence</a> has all products.',
+	'Each slice category has finite products and is essentially finite, hence has all products by <a href="/category-implication/freyd_finite">this result</a> followed by <a href="/category-implication/thin_finite_product_reduction">this result</a>.',
 	FALSE
 ),
 (
@@ -223,20 +209,6 @@ VALUES
 	'If $X_1,X_2,\dotsc$ is an infinite sequence of objects, then their product is the limit of the sequence $\cdots \to X_2 \times X_1 \to X_1$.',
 	FALSE
 ),
-(
-	'products_include_powers',
-	'["products"]',
-	'["powers"]',
-	'This is trivial.',
-	FALSE
-),
-(
-	'countable_products_include_countable_powers',
-	'["countable products"]',
-	'["countable powers"]',
-	'This is trivial.',
-	FALSE
-),
 (
 	'finite_products_include_finite_powers',
 	'["finite products"]',
@@ -251,13 +223,6 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
-(
-	'empty_power',
-	'["finite powers"]',
-	'["terminal object"]',
-	'The empty power is a terminal object.',
-	FALSE
-),
 (
 	'powers_include_countable_powers',
 	'["powers"]',
@@ -273,9 +238,9 @@ VALUES
 	FALSE
 ),
 (
-	'finite_powers_include_binary_powers',
+	'finite_powers_consequences',
 	'["finite powers"]',
-	'["binary powers"]',
+	'["binary powers", "terminal object"]',
 	'This is trivial.',
 	FALSE
 ),

diff --git a/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql
@@ -196,17 +196,10 @@ VALUES
 	FALSE
 ),
 (
-	'extensive_strict',
+	'extensive_consequences',
 	'["extensive"]',
-	'["strict initial object"]',
-	'This is Prop. 2.8 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.',
-	FALSE
-),
-(
-	'extensive_consequence',
-	'["extensive"]',
-	'["disjoint finite coproducts"]',
-	'This is Prop. 2.6 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.',
+	'["disjoint finite coproducts", "strict initial object"]',
+	'These are Prop. 2.6 and 2.8 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.',
 	FALSE
 ),
 (
@@ -230,13 +223,6 @@ VALUES
 	'This holds by definition of a regular category.',
 	FALSE
 ),
-(
-	'lextensive_def',
-	'["lextensive"]',
-	'["extensive", "finitely complete"]',
-	'This holds by definition.',
-	TRUE
-),
 (
 	'power_construction',
 	'["copowers", "cartesian closed"]',

diff --git a/database/data/005_implications/003_size-constraints-implications.sql b/database/data/005_implications/003_size-constraints-implications.sql
@@ -14,9 +14,9 @@ VALUES
 	FALSE
 ),
 (
-	'essentially_small_consequence',
+	'essentially_small_consequences',
 	'["essentially small"]',
-	'["well-powered", "well-copowered", "locally essentially small"]',
+	'["well-powered", "well-copowered", "locally essentially small", "generating set"]',
 	'This is trivial.',
 	FALSE
 ),
@@ -69,13 +69,6 @@ VALUES
 	'If $S$ is a generating set, we claim that $U := \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.',
 	FALSE
 ),
-(
-	'generating_set_small_categories',
-	'["essentially small"]',
-	'["generating set"]',
-	'In a small category, the set of all objects is clearly a generating set.',
-	FALSE
-),
 (
 	'free-algebra-generates',
 	'["finitary algebraic"]',

diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql
@@ -8,9 +8,9 @@ INSERT INTO implication_input (
 VALUES
 (
 	'cancellative_consequence',
-	'["left cancellative", "coequalizers"]',
+	'["right cancellative", "equalizers"]',
 	'["thin"]',
-	'If $f,g$ are two parallel morphisms, then their coequalizer is a regular epimorphism, but also a monomorphism by assumption, so it must be an isomorphism. But this means that $f = g$.',
+	'If $f,g$ are two parallel morphisms, then their equalizer is a regular monomorphism, but also an epimorphism by assumption, so it must be an isomorphism. But this means that $f = g$.',
 	FALSE
 ),
 (
@@ -55,34 +55,6 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
-(
-	'groupoid_thin',
-	'["groupoid", "equalizers"]',
-	'["thin"]',
-	'The equalizer of any parallel pair $f,g$ must be an isomorphism, so $f=g$.',
-	FALSE
-),
-(
-	'groupoid_products',
-	'["groupoid", "binary products", "inhabited"]',
-	'["trivial"]',
-	'Let $\mathcal{C}$ be an inhabited groupoid with binary products. Then it is connected, so we may assume $\mathcal{C}=BG$ for a group $G$ with unique object $*$. But then $* \times * = *$, so there are $p,q \in G$ such that $G \to G \times G$, $x \mapsto (px,qx)$ is bijective. From here it is an easy exercise to deduce $G=1$.',
-	FALSE
-),
-(
-	'groupoid_initial',
-	'["groupoid", "initial object"]',
-	'["trivial"]',
-	'This is easy.',
-	FALSE
-),
-(
-	'groupoid_zero',
-	'["groupoid", "zero morphisms", "inhabited"]',
-	'["trivial"]',
-	'This is easy.',
-	FALSE
-),
 (
 	'groupoid_connected',
 	'["groupoid", "connected"]',
@@ -167,13 +139,6 @@ VALUES
 	'If $f,g : A \rightrightarrows B$ are two morphisms, then $f^{-1} \circ g : A \to A$ must be the identity, so that $f = g$.',
 	FALSE
 ),
-(
-	'discrete_implies_direct',
-	'["discrete"]',
-	'["direct"]',
-	'This is trivial.',
-	FALSE
-),
 (
 	'direct_implies_sequential_limits',
 	'["direct"]',