add missing reasons for Rel

ScriptRaccoon · ScriptRaccoon · commit 61b5b4f813c2 · 2026-03-21T13:52:18.000+01:00
diff --git a/database/data/008_category-unsatisfied-properties.sql b/database/data/008_category-unsatisfied-properties.sql
@@ -349,12 +349,12 @@ VALUES
 	(
 		'Rel',
 		'preadditive',
-		NULL
+		'In categories with finite products and coproducts, the preadditive structure is <i>unique</i>: If $f,g : A \to B$ are morphisms, their sum $f+g : A \to B$ is the composite of $(f,g) : A \to B \times B$, the inverse of the canonical morphism $B \oplus B \to B \times B$ (which indeed must be an isomorphism), and the codiagonal $B \oplus B \to B$. In the case of $\mathbf{Rel}$, where both products and coproducts are just disjoint unions, this operation is just the set-theoretic union $f+g = f \cup g$ of relations. This clearly has no inverses.'
 	),
 	(
 		'Rel',
 		'Cauchy complete',
-		NULL
+		'See <a href="https://math.stackexchange.com/a/5030380/1650" target="_blank">MSE/1931577</a>.'
 	),
 	(
 		'Rel',

Original file line number	Diff line number	Diff line change
`@@ -349,12 +349,12 @@ VALUES`
`349`	`349`	`(`
`350`	`350`	`'Rel',`
`351`	`351`	`'preadditive',`
`352`		`- NULL`
	`352`	+ 'In categories with finite products and coproducts, the preadditive structure is <i>unique</i>: If $f,g : A \to B$ are morphisms, their sum $f+g : A \to B$ is the composite of $(f,g) : A \to B \times B$, the inverse of the canonical morphism $B \oplus B \to B \times B$ (which indeed must be an isomorphism), and the codiagonal $B \oplus B \to B$. In the case of $\mathbf{Rel}$, where both products and coproducts are just disjoint unions, this operation is just the set-theoretic union $f+g = f \cup g$ of relations. This clearly has no inverses.'
`353`	`353`	`),`
`354`	`354`	`(`
`355`	`355`	`'Rel',`
`356`	`356`	`'Cauchy complete',`
`357`		`- NULL`
	`357`	`+ 'See <a href="https://math.stackexchange.com/a/5030380/1650" target="_blank">MSE/1931577</a>.'`
`358`	`358`	`),`
`359`	`359`	`(`
`360`	`360`	`'Rel',`