Reorganize proofs of implications from cancellativity

Author: dschepler

databases/catdat/data/005_implications/001_limits-colimits-existence-implications.sql

@@ -76,20 +76,6 @@ VALUES
 	'In a thin category, any congruence pair is a reflexive fork, and thus consists of equal isomorphisms. Therefore, the congruence is the kernel pair of the identity morphism on the target.',
 	FALSE
 ),
-(
-	'left_cancellative_effective_congruences',
-	'["left cancellative"]',
-	'["effective congruences"]',
-	'For any congruence $f, g : E \rightrightarrows X$, if $r$ is the reflexivity morphism we have $r$ is both an epimorphism and a split monomorphism, so it is an isomorphism. Therefore, $f\circ r = g\circ r = \mathrm{id}_X$ implies $f = g$.  As <a href="core-hin_quotients">here</a>, that implies that $E$ is the kernel pair of $\mathrm{id}_X$.',
-	FALSE
-),
-(
-	'right_cancellative_effective_congruences',
-	'["right cancellative"]',
-	'["effective congruences"]',
-	'For any congruence $f, g : E \rightrightarrows X$, if $r$ is the reflexivity morphism we have $f\circ r = g\circ r = \mathrm{id}_X$, so $f = g$.  As <a href="core-hin_quotients">here</a>, that implies that $E$ is the kernel pair of $\mathrm{id}_X$.',
-	FALSE
-),
 (
 	'products_consequences',
 	'["products"]',

databases/catdat/data/005_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
 ),
 (