Has effective (co)congruences properties

databases/catdat/data/002_category-properties/001_limits-colimits-existence.sql

@@ -343,6 +343,38 @@ VALUES
 	'quotients of congruences',
 	TRUE
 ),
+(
+	'effective congruences',
+	'has',
+	'A congruence $f, g : E \rightrightarrows X$ (see definition <a href="/category-property/quotients_of_congruences">here</a>) is <i>effective</i> if it is the kernel pair of some morphism, i.e. if there is a morphism $h : X \to Y$ such that we have a cartesian square
+	$$
+	\begin{CD}
+	E @> f >> X \\
+	@V g VV @V h VV \\
+	X @> h >> Y.
+	\end{CD}
+	$$
+	A category <i>has effective congruences</i> if every congruence in the category is effective.',
+	'https://ncatlab.org/nlab/show/congruence',
+	'effective cocongruences',
+	TRUE
+),
+(
+	'effective cocongruences',
+	'has',
+	'A cocongruence $f, g : X \rightrightarrows E$ (see definition <a href="/category-property/coquotients_of_cocongruences">here</a>) is <i>effective</i> if it is the cokernel pair of some morphism, i.e. if there is a morphism $h : Y \to X$ such that we have a cocartesian square
+	$$
+	\begin{CD}
+	Y @> h >> X \\
+	@V h VV @V f VV \\
+	X @> g >> E.
+	\end{CD}
+	$$
+	A category <i>has effective cocongruences</i> if every cocongruence in the category is effective.',
+	NULL,
+	'effective congruences',
+	TRUE
+),
 (
 	'cosifted limits',
 	'has',

databases/catdat/data/002_category-properties/100_related-category-properties.sql

@@ -291,9 +291,17 @@ VALUES
 ('quotients of congruences', 'coequalizers'),
 ('quotients of congruences', 'cokernels'),
 ('quotients of congruences', 'regular'),
+('quotients of congruences', 'effective congruences'),
 ('coquotients of cocongruences', 'equalizers'),
 ('coquotients of cocongruences', 'kernels'),
 ('coquotients of cocongruences', 'coregular'),
+('coquotients of cocongruences', 'effective cocongruences'),
+('effective congruences', 'normal'),
+('effective congruences', 'quotients of congruences'),
+('effective congruences', 'mono-regular'),
+('effective cocongruences', 'conormal'),
+('effective cocongruences', 'coquotients of cocongruences'),
+('effective cocongruences', 'epi-regular'),
 ('direct', 'one-way'),
 ('direct', 'skeletal'),
 ('inverse', 'one-way'),
@@ -339,13 +347,17 @@ VALUES
 ('cofiltered', 'finitely complete'),
 ('cofiltered', 'cofiltered limits'),
 ('mono-regular', 'normal'),
+('mono-regular', 'effective congruences'),
 ('epi-regular', 'conormal'),
+('epi-regular', 'effective cocongruences'),
 ('normal', 'zero morphisms'),
 ('normal', 'mono-regular'),
 ('normal', 'kernels'),
+('normal', 'effective congruences'),
 ('conormal', 'zero morphisms'),
 ('conormal', 'epi-regular'),
 ('conormal', 'cokernels'),
+('conormal', 'effective cocongruences'),
 ('multi-complete', 'complete'),
 ('multi-complete', 'multi-terminal object'),
 ('multi-terminal object', 'multi-complete'),

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

@@ -65,6 +65,12 @@ VALUES
 	TRUE,
 	'The proof works exactly as for the <a href="/category/FinSet">category of finite sets</a>.'
 ),
+(
+	'FinGrp',
+	'effective congruences',
+	TRUE,
+	'For a kernel pair $E$ of $h : X \to Z$ where $E$ and $X$ are finite groups, replacing $Z$ with the image of $h$ gives the same kernel pair.'
+),
 (
 	'FinGrp',
 	'normal',
@@ -118,4 +124,4 @@ VALUES
 	'countable',
 	FALSE,
 	'This is trivial.'
-);
+);

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

@@ -61,6 +61,12 @@ VALUES
 	(1) If $f : A \to B$ is surjective, it is the coequalizer of $A \times_B A \rightrightarrows A$ in $\mathbf{Ab}$. Since $A \times_B A$ is free abelian, $f$ is also an coequalizer in $\mathbf{FreeAb}$.<br>
 	(2) If $f : A \to B$ is a regular epimorphism in $\mathbf{FreeAb}$, consider the factorization $f = i \circ p$ as above. Since $f$ is an extremal epimorphism, $i$ must be an isomorphism, so that $f$ is surjective.'
 ),
+(
+	'FreeAb',
+	'effective cocongruences',
+	TRUE,
+	'Since $\mathbf{Ab}$ is abelian, it has effective cocongruences. Now, suppose a cocongruence $X \rightrightarrows E$ is the cokernel pair of $h : Z \to X$, where $X$ and $E$ are free abelian groups. If we find a surjective map $g : F \to Z$ where $F$ is a free abelian group, then $h \circ g$ has the same cokernel pair as $h$, and $h \circ g$ is a morphism in $\mathbf{FreeAb}$.'
+),
 (
 	'FreeAb',
 	'countable powers',
@@ -84,4 +90,4 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509715" target="_blank">MO/509715</a>.'
-);
+);

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

@@ -47,6 +47,12 @@ VALUES
 	TRUE,
 	'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for groups.'
 ),
+(
+	'Grp',
+	'effective cocongruences',
+	TRUE,
+	'A proof can be found <a href="/pdf/cocongruences_of_groups.pdf">here</a>.'
+),
 (
 	'Grp',
 	'normal',

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

@@ -80,6 +80,12 @@ VALUES
 	Because $r \circ (p \circ i_1) : X \to X$ is the identity, the image of $p \circ i_1$ is the equalizer of $\mathrm{id}_E$ and $(p \circ i_1) \circ r$, hence closed. Likewise, the image of $p \circ i_2$ is closed. Thus, the image of $p$, which is the union of these images, is closed.<br>
 	Now, since the pushforward maps of tangent spaces compose to the identity, we see that $p$ must be a local immersion and $r$ must be a submersion.  Also, since the fibers of $r$ have one or two points each, we see that the dimension of $E$ must locally be the same as the dimension of $X$.  This implies that in fact $p$ and $r$ are local diffeomorphisms.  Therefore, the cardinality of the fiber of $r$ is locally constant.  Thus, if $U$ is the subset of $X$ where $r$ has fiber of a single point, with the subspace topology, then $U$ is a clopen submanifold of $X$ which serves as the equalizer of $p \circ i_1$ and $p \circ i_2$.'
 ),
+(
+	'Man',
+	'effective cocongruences',
+	TRUE,
+	'From the proof that $\mathbf{Man}$ has coquotients of cocongruences, we know that for any cocongruence $X \rightrightarrows E$, there is a clopen submanifold $U$ of $X$ such that the fibers of $r : E \twoheadrightarrow X$ have one point on $U$, and two points on $X \setminus U$. Therefore, $E$ is the cokernel pair of the inclusion map $U \hookrightarrow X$.'
+),
 (
 	'Man',
 	'small',

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

@@ -100,4 +100,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\mathbf{Set} \to \mathbf{Meas}$ which equips a set with the trivial $\sigma$-algebra.'
+),
+(
+	'Meas',
+	'effective cocongruences',
+	FALSE,
+	'The proof is similar to the one for <a href="/category/Top">$\mathbf{Top}$</a>: Use the trivial $\sigma$-algebra on a two-point space.'
 );

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

@@ -144,4 +144,10 @@ VALUES
 	'If $(N,z,s)$ is a natural numbers object in $\mathbf{Met}$, then
 	$$1 \xrightarrow{z} N \xleftarrow{s} N$$
 	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
-);
+),
+(
+	'Met',
+	'effective congruences',
+	FALSE,
+	'Any kernel pair of $h : X \to Z$ in $\mathbf{Met}$ corresponds to a closed subset of $X\times X$. However, there are plenty of non-closed congruences, such as $\Delta \cup (\mathbb{Q} \times \mathbb{Q}) \subseteq \mathbb{R} \times \mathbb{R}$ with the subspace metric.'
+);

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

@@ -138,4 +138,10 @@ VALUES
 	'If $(N,z,s)$ is a natural numbers object in $\mathbf{PMet}$, then
 	$$1 \xrightarrow{z} N \xleftarrow{s} N$$
 	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
+),
+(
+	'PMet',
+	'effective cocongruences',
+	FALSE,
+	'The proof is similar to the one for <a href="/category/Top">$\mathbf{Top}$</a>: Use the two-point space with the zero metric, which represents the functor taking a pseudo-metric space to the pairs of points with $d(x,y) = 0$. In this case, once you conclude $Z = \varnothing$, the map $h : Z \to 1$ does not have any cokernel pair, since that would have to be a coproduct $1+1$.'
 );

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

@@ -100,4 +100,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to \mathbf{Prost}$ that equips a set with the chaotic preorder.'
+),
+(
+	'Prost',
+	'effective cocongruences',
+	FALSE,
+	'Consider the proset $E := \{ a, b \}$ with the chaotic preorder. This represents the functor which sends a proset to the pairs of elements $x,y$ with $x \le y$ and $y \le x$. Therefore, it defines a cocongruence $1 \rightrightarrows E$, where the maps are the two possible functions. However, this cannot be effective: for any map $h : Z \to 1$ which equalizes the two functions, $Z$ must be empty. But that means the cokernel pair of $h$ is the two-element proset with the trivial preorder.'
 );

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

@@ -71,6 +71,12 @@ VALUES
 	TRUE,
 	'A proof can be found <a href="/pdf/congruences_in_rel.pdf">here</a>.'
 ),
+(
+	'Rel',
+	'effective congruences',
+	TRUE,
+	'A proof can be found <a href="/pdf/congruences_in_rel.pdf">here</a>.'
+),
 (
 	'Rel',
 	'preadditive',

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

@@ -77,6 +77,12 @@ VALUES
 	TRUE,
 	'This is because $\{0,1\}$ is a subobject classifier in $\mathbf{Set}$, which is countable, and the monomorphisms coincide.'
 ),
+(
+	'Set_c',
+	'effective congruences',
+	TRUE,
+	'For a kernel pair $E$ of $h : X \to Z$ where $E$ and $X$ are countable, replacing $Z$ with the image of $h$ gives the same kernel pair.'
+),
 (
 	'Set_c',
 	'small',

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

@@ -41,6 +41,18 @@ VALUES
 	TRUE,
 	'A congruence on a set $X$ in $\mathbf{Set}_\mathrm{f}$ is the same as an equivalence relation $R$ on $X$ whose equivalence classes are finite. In that case, the usual quotient map $p : X \to X/R$ is finite-to-one. Moreover, if $h : X/R \to Y$ is a map such that $h \circ p : X \to Y$ is finite-to-one, then $h$ is finite-to-one as well because $h^*(\{y\}) \subseteq p^*((h \circ p)^*(\{y\}))$ for all $y \in Y$. Therefore, $p$ is also the quotient in $\mathbf{Set}_\mathrm{f}$.'
 ),
+(
+	'Set_f',
+	'effective congruences',
+	TRUE,
+	'If $E \rightrightarrows X$ is the kernel pair of $h : X \to Z$ in $\mathbf{Set}$ and both maps $E \to X$ are finite-to-one, then that means the equivalence classes of $E$ are finite. Thus, necessarily $h$ was finite-to-one also.'
+),
+(
+	'Set_f',
+	'effective cocongruences',
+	TRUE,
+	'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\mathbf{Set}_f$. Then it is a coreflexive corelation in $\mathbf{Set}$. Since $\mathbf{Set}$ is co-Malcev and has effective cocongruences, that implies $E$ is the cokernel pair of some function $h : Z \to X$. If we replace $h$ with the inclusion map of its image, then this function is in $\mathbf{Set}_\mathrm{f}$ and gives the same cokernel pair.'
+),
 (
 	'Set_f',
 	'locally cartesian closed',
@@ -132,4 +144,4 @@ VALUES
 	FALSE,
 	'We will prove that the family of singleton sets $(1)_{n \in \mathbb{N}}$ has no multi-coproduct, generalizing the proof that the family does not have a coproduct given above. A cocone is just a map of sets $f : \mathbb{N} \to X$. A morphism from $f : \mathbb{N} \to X$ to $g : \mathbb{N} \to Y$ is a finite-to-one map $h : X \to Y$ with $g = h \circ f$. This describes the category of cocones, and we need to show that it has no multi-initial object. To this end, we claim that the connected component of the unique map $! : \mathbb{N} \to 1$ consists precisely of the maps $f : \mathbb{N} \to X$ with finite image. Once that is established, we can recycle the proof for missing coproducts since there we have only used finite codomains.<br>
 	Let $g = h \circ f$ be as above. If $\mathrm{im}(f)$ is finite, then $\mathrm{im}(g) = h_*(\mathrm{im}(f))$ is finite as well. Conversely, if $\mathrm{im}(g)$ is finite, then $\mathrm{im}(f) \subseteq \bigcup_{y \in \mathrm{im}(g)} h^*(\{y\})$ is finite as well. This shows that the connected component of $!$ is contained in the collection of maps with finite image. Conversely, if $f$ has finite image, then there is a morphism from the corestriction $f'' : \mathbb{N} \to \mathrm{im}(f)$ to $f$, and also a morphism from $f''$ to $!$. This proves the remaining inclusion.'
-);
+);

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

@@ -67,6 +67,13 @@ VALUES
 	TRUE,
 	'The coproduct (wedge sum) of a family of pointed sets $(X_i)_{i \in I}$ can be realized as the subset of $\prod_{i \in I} X_i$ consisting of those tuples $x$ such that $x_i = 0$ for all but (at most) one index.'
 ),
+(
+	-- TODO: rework this when Barr-exact is added
+	'Set*',
+	'effective cocongruences',
+	TRUE,
+	'We have that $\mathbf{Set}_*^{\mathrm{op}}$ is a slice category of $\mathbf{Set}^{\mathrm{op}}$, which in turn is monadic over $\mathbf{Set}$. Therefore, by combining results from <a href="http://www.springer.com/us/book/9781402019616" target="_blank">Borceux and Bourn</a> Appendix A and <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact" target="_blank">nLab</a>, $\mathbf{Set}_*^{\mathrm{op}}$ is Barr-exact, and in particular it has effective congruences.'
+),
 (
 	'Set*',
 	'skeletal',

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

@@ -114,6 +114,12 @@ VALUES
 	TRUE,
 	'This follows from <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor to $\mathbf{Set}$.'
 ),
+(
+	'Setne',
+	'effective congruences',
+	TRUE,
+	'If a congruence $E \rightrightarrows X$ is the kernel pair of $h : X \to Z$, with both $E$ and $X$ non-empty, then certainly $Z$ must also be non-empty.'
+),
 (
 	'Setne',
 	'sequential limits',
@@ -137,4 +143,11 @@ VALUES
 	'coquotients of cocongruences',
 	FALSE,
 	'The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ &mdash; namely the cofull cocongruence on $\{0\}$ &mdash; but they do not have an equalizer.'
-)
+),
+(
+	'Setne',
+	'effective cocongruences',
+	FALSE,
+	'The two maps $\{0\} \rightrightarrows \{0,1\}$ form a cocongruence on $\{0\}$ &mdash; namely the cofull cocongruence on $\{0\}$ &mdash; but there is no map $Z \to \{0\}$ making the required commutative diagram, much less a cocartesian square.'
+);
+

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

@@ -23,6 +23,12 @@ VALUES
     TRUE,
     'Take the two-sorted algebraic theory with no operations and no equations.'
 ),
+(
+	'SetxSet',
+	'effective cocongruences',
+	TRUE,
+	'Suppose we have a cocongruence $X \rightrightarrows E$ in $\mathbf{Set} \times \mathbf{Set}$. Then each component is a cocongruence, so they are the kernel pairs of some maps $Z_1\to X_1$, $Z_2 \to X_2$. Then $E$ is the cokernel pair of $(Z_1, Z_2) \to (X_1, X_2)$.'
+),
 (
 	'SetxSet',
 	'skeletal',

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

@@ -130,4 +130,10 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\mathbf{Set} \to \mathbf{Top}$ which equips a set with the indiscrete topology.'
+),
+(
+	'Top',
+	'effective cocongruences',
+	FALSE,
+	'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.'
 );

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

@@ -168,7 +168,16 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\mathbf{Set}_*$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\mathbf{Set}_* \to \mathbf{Top}_*$ that equips a pointed set with the indiscrete topology.'
+),
+(
+	'Top*',
+	'effective congruences',
+	FALSE,
+	'Suppose that $\mathbf{Top}_*$ had effective congruences. Then for any congruence $E \rightrightarrows X$ in $\mathbf{Top}$, we can expand it to a congruence $E + \{*\} \rightrightarrows X + \{*\}$ in $\mathbf{Top}_*$. If $E + \{*\}$ is the kernel pair of $h : X + \{*\} \to Z$, then $E$ is the kernel pair of $h$ restricted to $X$. This contradicts the fact that $\mathbf{Top}$ does not have effective congruences.'
+),
+(
+	'Top*',
+	'effective cocongruences',
+	FALSE,
+	'Consider the pointed topological space $I := \{ *, a, b \}$ with topology $\{ \varnothing, \{ * \}, \{ a, b \}, \{ *, a, b \} \}$. This represents the functor which sends a pointed topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $\{ *, a \} \rightrightarrows I$ on the discrete space $\{ *, a \}$, where the maps are the two possible pointed functions. However, this cannot be effective: if we have $h : Z \to \{ *, a \}$ which equalizes the cocongruence, then $Z$ must be the singleton pointed space. But that means the cokernel pair of $h$ is the discrete space on $\{ *, a, b \}$.'
 );
-
-
-

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

@@ -53,6 +53,18 @@ VALUES
 	TRUE,
 	'This follows immediately from the fact for $\mathbf{Set}$.'
 ),
+(
+	'Z',
+	'effective congruences',
+	TRUE,
+	'If we have a congruence $E \rightrightarrows X$ in $[\mathbf{CRing}, \mathbf{Set}]$, then each image at a commutative ring gives a congruence in $\mathbf{Set}$. Defining $Y$ pointwise to be the quotient of this congruence, we get a morphism of functors $h : X \to Y$ whose kernel pair is $E$.'
+),
+(
+	'Z',
+	'effective cocongruences',
+	TRUE,
+	'If we have a congruence $X\rightrightarrows E$ in $[\mathbf{CRing}, \mathbf{Set}]$, then each image at a commutative ring gives a cocongruence in $\mathbf{Set}$. Defining $Y$ pointwise to be the equalizer of the pair, we get a morphism of functors $h : Y \to X$ whose cokernel pair is $E$.'
+),
 (
 	'Z',
 	'locally essentially small',
@@ -100,4 +112,4 @@ VALUES
 	'cofiltered-limit-stable epimorphisms',
 	FALSE,
 	'We already know that $\mathbf{Set}$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the functor $\mathbf{Set} \to [\mathbf{CRing}, \mathbf{Set}]$ that maps a set to its constant functor.'
-);
+);

databases/catdat/data/004_category-implications/004_morphism-behavior-implications.sql

@@ -37,8 +37,8 @@ VALUES
 (
 	'reflexive_pair_trivial',
 	'["left cancellative"]',
-	'["reflexive coequalizers", "coreflexive equalizers"]',
-	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms.',
+	'["reflexive coequalizers", "coreflexive equalizers", "effective congruences", "effective cocongruences"]',
+	'Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of the identity morphism on the target, and the cokernel pair of the identity morphism on the source.',
 	FALSE
 ),
 (
@@ -178,8 +178,8 @@ VALUES
 (
 	'core-hin_quotients',
 	'["core-thin"]',
-	'["quotients of congruences"]',
-	'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\mathrm{id}_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\mathrm{id}_X$ is a coequalizer.',
+	'["quotients of congruences", "effective congruences"]',
+	'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\mathrm{id}_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\mathrm{id}_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \mathrm{id}$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \mathrm{id}$ and $p_2 \circ r \circ p_1 = p_2 \circ \mathrm{id}$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \mathrm{id}$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\mathrm{id}_X$.',
 	FALSE
 ),
 (
@@ -188,4 +188,4 @@ VALUES
 	'["skeletal", "core-thin"]',
 	'This is trivial.',
 	TRUE
-);
+);