prefer dual form

ScriptRaccoon · ScriptRaccoon · commit 2c200a389a36 · 2026-04-17T11:07:30.000+02:00
diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql
@@ -8,9 +8,9 @@ INSERT INTO implication_input (
 VALUES
 (
 	'cancellative_consequence',
-	'["left cancellative", "coequalizers"]',
+	'["right cancellative", "equalizers"]',
 	'["thin"]',
-	'If $f,g$ are two parallel morphisms, then their coequalizer is a regular epimorphism, but also a monomorphism by assumption, so it must be an isomorphism. But this means that $f = g$.',
+	'If $f,g$ are two parallel morphisms, then their equalizer is a regular monomorphism, but also an epimorphism by assumption, so it must be an isomorphism. But this means that $f = g$.',
 	FALSE
 ),
 (

Original file line number	Diff line number	Diff line change
`@@ -8,9 +8,9 @@ INSERT INTO implication_input (`
`8`	`8`	`VALUES`
`9`	`9`	`(`
`10`	`10`	`'cancellative_consequence',`
`11`		`- '["left cancellative", "coequalizers"]',`
	`11`	`+ '["right cancellative", "equalizers"]',`
`12`	`12`	`'["thin"]',`
`13`		`- 'If $f,g$ are two parallel morphisms, then their coequalizer is a regular epimorphism, but also a monomorphism by assumption, so it must be an isomorphism. But this means that $f = g$.',`
	`13`	`+ 'If $f,g$ are two parallel morphisms, then their equalizer is a regular monomorphism, but also an epimorphism by assumption, so it must be an isomorphism. But this means that $f = g$.',`
`14`	`14`	`FALSE`
`15`	`15`	`),`
`16`	`16`	`(`