Remove redundant topos_is_co-malcev implication, and move citation to the special case remark in the more general result.

Also, revise subobject_classifier_disallows_malcev conclusion to subobject-trivial, which is the condition that it reaches slightly more directly.

Author: dschepler

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

@@ -187,8 +187,7 @@ VALUES
 
 	Thus, we get that a morphism $h : X+X'' \to Z$ factors through $E$ if and only if $h(x) = h(x)$ for every generalized element $x \in X$; $h(y) = h(y'')$ for every $y \in Y$; $h(y'') = h(y)$ for every $y\in Y$; and $h(x'') = h(x'')$ for every $x \in X$. Clearly this is equivalent to $h(y) = h(y'')$ for every $y\in Y$, so in fact $E$ is the cokernel pair of $i_1 \circ \operatorname{inc}_Y$ and $i_2 \circ \operatorname{inc}_Y$. This means that $E$ is an effective cocongruence.<br><br>
 
-	Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev.
-	',
+	Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof of this special case is given later in A.5.17.',
 	FALSE
 ),
 (
@@ -217,18 +216,11 @@ VALUES
 	'The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the <a href="https://ncatlab.org/nlab/show/extensive+category" target="_blank">nLab</a>.',
 	FALSE
 ),
-(
-	'topos_is_co-malcev',
-	'["elementary topos"]',
-	'["co-Malcev"]',
-	'This is Example 2.2.18 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. An alternative proof is given later in A.5.17.',
-	FALSE
-),
 (
 	'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.)',
+	'["subobject-trivial"]',
+	'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. (From here, we can infer that the category is trivial.)',
 	FALSE
 ),
 (