Add a general result to help deducing CompHaus is well-copowered

Author: dschepler

databases/catdat/data/004_category-implications/002_limits-colimits-behavior-implications.sql

@@ -260,6 +260,13 @@ VALUES
 	'This holds by definition of a regular category.',
 	FALSE
 ),
+(
+	'regular_well-powered_well-copowered',
+	'["regular", "well-powered"]',
+	'["well-copowered"]',
+	'The regularity condition gives a bijection between quotients of $X$ and effective congruences on $X$, which is a subset of the subobjects of $X\times X$.',
+	FALSE
+),
 (
 	'power_construction',
 	'["copowers", "cartesian closed"]',
@@ -294,4 +301,4 @@ VALUES
 	'["CIP"]',
 	'Let $(X_i)_{i \in I}$ be a family of objects. For every finite subset $E \subseteq I$ the canonical morphism $\coprod_{i \in E} X_i = \prod_{i \in E} X_i \to \prod_{i \in I} X_i$ is a (split) monomorphism. Hence, their colimit is also a monomorphism, which is the canonical morphism $\coprod_{i \in I} X_i \to \prod_{i \in I} X_i$.',
 	FALSE
-);
+);