refine implication: malcev + subobject classifier => thin (=> trivial)

Author: ScriptRaccoon

databases/catdat/data/003_category-property-assignments/Set_c.sql

@@ -89,12 +89,6 @@ VALUES
 	FALSE,
 	'This is trivial.'
 ),
-(
-	'Set_c',
-	'Malcev',
-	FALSE,
-	'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.'
-),
 (
 	'Set_c',
 	'regular',

databases/catdat/data/004_category-implications/008_topos-theory-implications.sql

@@ -189,10 +189,10 @@ VALUES
 	FALSE
 ),
 (
-	'topos_is_never_malcev',
-	'["elementary topos", "Malcev"]',
-	'["trivial"]',
-	'The subobject classifier $\Omega$ is an internal Heyting algebra and hence an internal poset (see <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). The relation $\leq$ on $\Omega$ is reflexive, hence symmetric by assumption. But then $\bot \leq \top$ in $\Omega$ implies $\top \leq \bot$, and hence $\bot = \top$. This means $1 \cong 0$ and hence $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.',
+	'subobject_classifier_disallows_malcev',
+	'["subobject classifier", "Malcev"]',
+	'["thin"]',
+	'The subobject classifier $\Omega$ is an internal poset (cf. <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, IV.8). Concretely, the intersection of subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every monomorphism must be an isomorphism. Applying this to equalizers, we see that the category is thin. (And from here, we can infer that it is trivial.)',
 	FALSE
 ),
 (