Existence of reflexive coequalizers

CONTRIBUTING.md

@@ -93,7 +93,7 @@ When contributing new data (categories, functors, properties, implications), ple
 
 - **Atomic Implications**: Do not add implications that can be deduced from others. For example, do not add "complete => finite products" since it can be deduced from "complete => finitely complete" and "finitely complete => finite products". These are deduced automatically.
 
-- **No dual implications**: Implications are dualized automatically when applicable. For this reason, adding the category implication "finitely cocomplete => pushouts" is not necessary when "finitely complete => pullbacks" has already been added. Similarly, the functor implication "comonadic => left adjoint" is automatically dualized from "monadic => right adjoint".
+- **No dual implications**: Implications are dualized automatically when applicable. For this reason, adding the category implication "finitely cocomplete => pushouts" is not necessary when "finitely complete => pullbacks" has already been added. Similarly, the functor implication "comonadic => left adjoint" is automatically dualized from "monadic => right adjoint". When an implication can be phrased both in a "limit" or "colimit" variant, prefer the "limit" variant (unless the literature focusses on the "colimit" variant).
 
 - **Relevant implications**: When adding a new property, include implications involving this property and existing properties. For example, when adding the property of categories of having "countable products", also add the implication "countable products => finite products". Refactor existing implications if necessary. Ensure that for most categories and functors, it will be inferred if the property holds or not.
 

database/data/004_property-assignments/Setne.sql

@@ -107,12 +107,6 @@ VALUES
 	FALSE,
 	'Assume that the sequence of inclusions $\cdots \to \mathbb{N}_{\geq 2} \to \mathbb{N}_{\geq 1} \to \mathbb{N}_{\geq 0} = \mathbb{N}$ as a limit $X$, consisting of maps $X \to \mathbb{N}_{\geq n}$. Since $X$ is non-empty, there is a map $1 \to X$. This corresponds to a family of compatible maps $ 1 \to \mathbb{N}_{\geq n}$, i.e. to compatible elements in $\mathbb{N}_{\geq n}$. But the set $\bigcap_{n \geq 0} \mathbb{N}_{\geq n}$ is empty.'
 ),
-(
-	'Setne',
-	'coreflexive equalizers',
-	FALSE,
-	'The two distinct functions $1 \rightrightarrows \{0,1\}$ have a (unique) common retraction, but they cannot extend to a fork.'
-),
 (
 	'Setne',
 	'skeletal',

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

@@ -35,12 +35,19 @@ VALUES
 	FALSE
 ),
 (
-	'reflexive_coequalizers_are_coequalizers',
-	'["coequalizers"]',
-	'["reflexive coequalizers"]',
+	'coreflexive_equalizers_are_equalizers',
+	'["equalizers"]',
+	'["coreflexive equalizers"]',
 	'This is trivial.',
 	FALSE
 ),
+(
+	'equalizers_via_coreflexive_equalizers',
+	'["coreflexive equalizers", "binary products"]',
+	'["equalizers"]',
+	'If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\mathrm{id}_X,f), (\mathrm{id}_X,g) : X \rightrightarrows X \times Y$. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\mathrm{id}_X,f)$ and $(\mathrm{id}_X,g)$. Thus, their equalizers agree.',
+	FALSE
+),
 (
 	'products_consequence',
 	'["products"]',
@@ -100,8 +107,8 @@ VALUES
 (
 	'complete_characterization',
 	'["complete"]',
-	'["products", "coreflexive equalizers"]',
-	'See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Thm. 2. Note that the equalizer appearing the theorem is in fact coreflexive.',
+	'["products", "equalizers"]',
+	'See <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, V.2, Thm. 2.',
 	TRUE
 ),
 (