From 5025e9d1ae3312895ea139b1a4aff1f2d9e5f225 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 08:43:41 -0400 Subject: [PATCH 01/14] Initial addition of Barr-exact, Barr-coexact, pretopos properties and some implications --- .../003_limits-colimits-behavior.sql | 18 +++++++++++++++- .../006_additional-structure.sql | 10 ++++++++- .../data/003_properties/009_topos-theory.sql | 10 ++++++++- .../data/004_property-assignments/Set.sql | 6 ++++++ ..._limits-colimits-behavior-implications.sql | 9 +++++++- .../005_additional-structure-implications.sql | 21 ++++++++++++------- .../006_trivial-categories-implications.sql | 8 +++---- .../008_topos-theory-implications.sql | 20 +++++++++++++++--- 8 files changed, 84 insertions(+), 18 deletions(-) diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 208234c7..89d89979 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -196,6 +196,22 @@ VALUES 'infinitary extensive', TRUE ), +( + 'Barr-exact', + 'is', + 'A category is Barr-exact if it is regular, and in addition, every internal equivalence relation is a kernel pair.', + 'https://ncatlab.org/nlab/show/exact', + 'Barr-coexact', + TRUE +), +( + 'Barr-coexact', + 'is', + 'A category is Barr-coexact if its dual is Barr-exact, i.e. it is coregular, and in addition, every internal equivalence corelation is a cokernel pair.', + NULL, + 'Barr-exact', + TRUE +), ( 'unital', 'is', @@ -211,4 +227,4 @@ VALUES NULL, 'unital', TRUE -); \ No newline at end of file +); diff --git a/database/data/003_properties/006_additional-structure.sql b/database/data/003_properties/006_additional-structure.sql index ace56231..3ce58f28 100644 --- a/database/data/003_properties/006_additional-structure.sql +++ b/database/data/003_properties/006_additional-structure.sql @@ -62,4 +62,12 @@ VALUES 'https://ncatlab.org/nlab/show/Grothendieck+category', NULL, TRUE -); \ No newline at end of file +), +( + 'monadically concrete', + 'is', + 'A category is monadically concrete if there exists a monadic functor to Set. Note this is not standard terminology, but is used in the CatDat system for its numerous implications.', + NULL, + NULL, + TRUE +); diff --git a/database/data/003_properties/009_topos-theory.sql b/database/data/003_properties/009_topos-theory.sql index 9fa4ca54..70bd4cae 100644 --- a/database/data/003_properties/009_topos-theory.sql +++ b/database/data/003_properties/009_topos-theory.sql @@ -83,6 +83,14 @@ VALUES 'regular subobject classifier', TRUE ), +( + 'pretopos', + 'is a', + 'A pretopos is a category which is both Barr-exact and extensive.', + 'https://ncatlab.org/nlab/show/pretopos', + NULL, + TRUE +), ( 'elementary topos', 'is an', @@ -109,4 +117,4 @@ VALUES 'https://ncatlab.org/nlab/show/natural+numbers+object', NULL, TRUE -); \ No newline at end of file +); diff --git a/database/data/004_property-assignments/Set.sql b/database/data/004_property-assignments/Set.sql index 8e266208..84a804a1 100644 --- a/database/data/004_property-assignments/Set.sql +++ b/database/data/004_property-assignments/Set.sql @@ -40,4 +40,10 @@ VALUES 'Malcev', FALSE, 'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.' +), +( + 'Set_op', + 'monadically concrete', + TRUE, + 'The contravariant powerset functor $\mathsf{Set}^{\operatorname{op}} \to \mathsf{Set}$ is monadic.' ); diff --git a/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql index 26cc5805..619f5dac 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/database/data/005_implications/002_limits-colimits-behavior-implications.sql @@ -251,6 +251,13 @@ VALUES 'This holds by definition of a regular category.', FALSE ), +( + 'barr_exact_def', + '["Barr-exact"]', + '["regular"]', + 'By definition', + FALSE +), ( 'power_construction', '["copowers", "cartesian closed"]', @@ -268,4 +275,4 @@ VALUES '["countable powers"]', 'We can recycle this proof.', FALSE -); \ No newline at end of file +); diff --git a/database/data/005_implications/005_additional-structure-implications.sql b/database/data/005_implications/005_additional-structure-implications.sql index 97962495..2b475c9c 100644 --- a/database/data/005_implications/005_additional-structure-implications.sql +++ b/database/data/005_implications/005_additional-structure-implications.sql @@ -7,10 +7,17 @@ INSERT INTO implication_input ( ) VALUES ( - 'finitary_algebraic_consequence', + 'finitary_algebraic_consequences', '["finitary algebraic"]', - '["locally strongly finitely presentable"]', - 'This is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras.', + '["locally strongly finitely presentable", "monadically concrete"]', + 'The first is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras. For the second, the forgetful functor to Set is monadic because the corresponding monad on Set takes a set to the collection of formal expressions in those variables modulo provable equality, and so it is easy to see an equivalence between an algebra over that monad and a model of the algebraic theory.', + FALSE +), +( + 'monadically_concrete_consequences', + '["monadically concrete"]', + '["complete", "Barr-exact"]', + 'It is complete because a monadic functor creates limits. It is Barr-exact because any Eilenberg-Moore category of a functor on Set is Barr-exact.', FALSE ), ( @@ -49,10 +56,10 @@ VALUES TRUE ), ( - 'abelian_implies_regular', + 'abelian_implies_exact', '["abelian"]', - '["regular"]', - 'In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see Mac Lane, Ch. VIII.', + '["Barr-exact"]', + 'In an abelian category, every epimorphism is regular, and epimorphisms are pullback-stable, see Mac Lane, Ch. VIII. This shows the category is regular. For exactness, strict quotients of internal equivalence relations can be constructed as cokernels.', FALSE ), ( @@ -110,4 +117,4 @@ VALUES '["trivial"]', 'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, Abelian categories, p. 116.', FALSE -); \ No newline at end of file +); diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index 6ad51eb0..2008453a 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/database/data/005_implications/006_trivial-categories-implications.sql @@ -119,10 +119,10 @@ VALUES FALSE ), ( - 'thin_implies_regular', + 'thin_implies_barr_exact', '["thin", "finitely complete"]', - '["regular"]', - 'In a thin category, regular epimorphisms are isomorphisms, and the rest is clear as well.', + '["Barr-exact"]', + 'In a thin category, regular epimorphisms are isomorphisms, and the rest of regularity is clear as well. For exactness, any internal equivalence relation (in fact any reflexive relation) is the full relation i.e. an isomorphism, and is therefore the kernel pair of the identity map.', FALSE ), ( @@ -152,4 +152,4 @@ VALUES '["exact filtered colimits"]', 'In a thin category, every (finite) limit can be reduced to a (finite) product.', FALSE -); \ No newline at end of file +); diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 8c2450f5..81363d2b 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -41,6 +41,13 @@ VALUES 'If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal.', FALSE ), +( + 'pretopos_definition', + '["pretopos"]', + '["Barr-exact", "extensive"]', + 'By definition.', + TRUE +), ( 'topos_definition', '["elementary topos"]', @@ -48,6 +55,13 @@ VALUES 'This holds by definition.', TRUE ), +( + 'topos_pretopos', + '["elementary topos"]', + '["pretopos"]', + 'All properties of a pretopos can be proved in a way similar to the way they are proved for Set, using the internal language and internal logic of an elementary topos.', + FALSE +), ( 'subobject_classifier_consequence', '["subobject classifier"]', @@ -121,8 +135,8 @@ VALUES ( 'topos_consequence', '["elementary topos"]', - '["finitely cocomplete", "disjoint finite coproducts", "epi-regular"]', - 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8.', + '["finitely cocomplete", "disjoint finite coproducts", "epi-regular", "Barr-coexact"]', + 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8. To see it is Barr-coexact, use that the contravariant power object functor is monadic and the topos itself is Barr-exact.', FALSE ), ( @@ -222,4 +236,4 @@ VALUES '["natural numbers object"]', 'The triple $(1, \mathrm{id}_1, \mathrm{id}_1)$ is clearly a NNO.', FALSE -); \ No newline at end of file +); From 6ce2fea8c7033955539aa20c3622f0733e1e63b2 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 09:42:45 -0400 Subject: [PATCH 02/14] Add a few assignments for Barr-exactness --- database/data/004_property-assignments/FinGrp.sql | 6 +++--- database/data/004_property-assignments/FreeAb.sql | 8 +++++++- database/data/004_property-assignments/Haus.sql | 7 +++++++ database/data/004_property-assignments/Met.sql | 2 +- database/data/004_property-assignments/Met_c.sql | 6 ++++++ database/data/004_property-assignments/Met_oo.sql | 6 ++++++ 6 files changed, 30 insertions(+), 5 deletions(-) diff --git a/database/data/004_property-assignments/FinGrp.sql b/database/data/004_property-assignments/FinGrp.sql index bf80a30b..c529488f 100644 --- a/database/data/004_property-assignments/FinGrp.sql +++ b/database/data/004_property-assignments/FinGrp.sql @@ -49,9 +49,9 @@ VALUES ), ( 'FinGrp', - 'regular', + 'Barr-exact', TRUE, - 'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.' + 'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. This shows the category is regular. For exactness, quotients of equivalence relations are inherited from Group, with a quotient of a finite group clearly being finite as well.' ), ( 'FinGrp', @@ -118,4 +118,4 @@ VALUES 'countable', FALSE, 'This is trivial.' -); \ No newline at end of file +); diff --git a/database/data/004_property-assignments/FreeAb.sql b/database/data/004_property-assignments/FreeAb.sql index 3be5d2a7..007a0db5 100644 --- a/database/data/004_property-assignments/FreeAb.sql +++ b/database/data/004_property-assignments/FreeAb.sql @@ -84,4 +84,10 @@ VALUES 'sequential colimits', FALSE, 'See MO/509715.' -); \ No newline at end of file +), +( + 'FreeAb', + 'Barr-exact', + FALSE, + 'Any kernel pair $E$ of a pair of morphisms to a free Abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$. However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.' +); diff --git a/database/data/004_property-assignments/Haus.sql b/database/data/004_property-assignments/Haus.sql index 6005cdf3..798fbc7d 100644 --- a/database/data/004_property-assignments/Haus.sql +++ b/database/data/004_property-assignments/Haus.sql @@ -94,4 +94,11 @@ VALUES 'regular subobject classifier', FALSE, 'Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\mathrm{Hom}(X,\Omega)$ and the set of closed subsets of $X$ for any Hausdorff space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\mathrm{Hom}(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' +), +( + 'Haus', + 'Barr-exact', + FALSE, + 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' ); + diff --git a/database/data/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index fcf2ab76..e737c9e9 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/database/data/004_property-assignments/Met.sql @@ -144,4 +144,4 @@ 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 Johnstone, 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 MSE/1778408.' -); \ No newline at end of file +); diff --git a/database/data/004_property-assignments/Met_c.sql b/database/data/004_property-assignments/Met_c.sql index 2dd5084b..e6cdd216 100644 --- a/database/data/004_property-assignments/Met_c.sql +++ b/database/data/004_property-assignments/Met_c.sql @@ -100,4 +100,10 @@ VALUES 'sequential colimits', FALSE, 'See MO/510316.' +), +( + 'Met_c', + 'Barr-exact', + FALSE, + 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' ); diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index 79cd4b3d..1f0ad8d6 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -82,4 +82,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509552: Consider the forgetful functor $U : \mathbf{Met}_{\infty} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(a,b) \in U(X)^2 : d(x,y) \leq 1 \}$. Both are representable: $U$ by the singleton metric space and $R$ by the metric space $\{ 0,1 \}$ where $d(0,1) := 1$. It is clear that $R$ is reflexive, but not transitive.' +), +( + 'Met_oo', + 'Barr-exact', + FALSE, + 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' ); From 380eb7f5e6e6effdbcd25891ac44496a540abb86 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 10:16:25 -0400 Subject: [PATCH 03/14] Resolve Barr-coexact for Set* --- database/data/004_property-assignments/Set_pointed.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/004_property-assignments/Set_pointed.sql b/database/data/004_property-assignments/Set_pointed.sql index a0719751..4d04aec6 100644 --- a/database/data/004_property-assignments/Set_pointed.sql +++ b/database/data/004_property-assignments/Set_pointed.sql @@ -43,9 +43,9 @@ VALUES ), ( 'Set*', - 'coregular', + 'Barr-coexact', TRUE, - 'From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for the category of sets and the observation that the forgetful functor $\mathbf{Set}_* \to \mathbf{Set}$ preserves pushouts.' + 'According to nLab with a citation to Borceux and Bourn, Appendix A, any slice or co-slice of a Barr-exact category is also Barr-exact. It follows that any slice or co-slice of a Barr-coexact category is also Barr-coexact, and $\mathbf{Set}_*$ is a coslice category of $\mathbf{Set}$, which is Barr-coexact since $\mathbf{Set}^{\operatorname{op}}$ is monadic over $\mathbf{Set}$.' ), ( 'Set*', From 12f60f90c8c2a4f029de62d4ee802321db010aad Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 10:19:27 -0400 Subject: [PATCH 04/14] Revert addition of Barr-coexact implication of elemetary topos - it turns out the proof on ncatlab for categories monadic over Set requires the external axiom of choice on Set, so it will only generalize to elemetary topoi with choice --- .../data/005_implications/008_topos-theory-implications.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 81363d2b..dcf9bd57 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -135,8 +135,8 @@ VALUES ( 'topos_consequence', '["elementary topos"]', - '["finitely cocomplete", "disjoint finite coproducts", "epi-regular", "Barr-coexact"]', - 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8. To see it is Barr-coexact, use that the contravariant power object functor is monadic and the topos itself is Barr-exact.', + '["finitely cocomplete", "disjoint finite coproducts", "epi-regular"]', + 'See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8.', FALSE ), ( From ec81faeb226d3d1aaaf2ff86b5bedc2ac8399616 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 10:22:56 -0400 Subject: [PATCH 05/14] Add manual resolution of Barr-coexact for Set --- database/data/004_property-assignments/Set.sql | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/database/data/004_property-assignments/Set.sql b/database/data/004_property-assignments/Set.sql index 84a804a1..b04f6277 100644 --- a/database/data/004_property-assignments/Set.sql +++ b/database/data/004_property-assignments/Set.sql @@ -29,6 +29,12 @@ VALUES TRUE, 'Use the empty algebraic theory.' ), +( + 'Set', + 'Barr-coexact', + TRUE, + '$\mathbf{Set}^{\operatorname{op}}$ is monadic over $\mathbf{Set}$.' +), ( 'Set', 'skeletal', From f9b9b73fb728c49ec69506b7b7deeae979b19676 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 11:29:23 -0400 Subject: [PATCH 06/14] Add a couple cases which were unresolved by removing the faulty implication topos->Barr-coexact, but are still cases of topoi with external axiom of choice --- database/data/004_property-assignments/FinSet.sql | 6 ++++++ database/data/004_property-assignments/SetxSet.sql | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index 3b91f482..885bcb01 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/database/data/004_property-assignments/FinSet.sql @@ -47,6 +47,12 @@ VALUES TRUE, 'The inclusion $\mathbf{FinSet} \hookrightarrow \mathbf{Set}$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\mathbf{Set}$, it is still ℵ₁-presentable in $\mathbf{FinSet}$. Therefore, $\mathbf{FinSet}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' ), +( + 'FinSet', + 'Barr-coexact', + TRUE, + 'If an equivalence corelation is a cokernel pair of $f, g : Y \to X$, then we can replace $Y$ with the appropriate equalizer which is finite.' +), ( 'FinSet', 'small', diff --git a/database/data/004_property-assignments/SetxSet.sql b/database/data/004_property-assignments/SetxSet.sql index d5c9beac..2fbdfa3d 100644 --- a/database/data/004_property-assignments/SetxSet.sql +++ b/database/data/004_property-assignments/SetxSet.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'Take the two-sorted algebraic theory with no operations and no equations.' ), +( + 'SetxSet', + 'Barr-coexact', + TRUE, + '$(\mathbf{Set} \times \mathbf{Set})^{\operatorname{op}}$ is monadic over $\mathbf{Set} \times \mathbf{Set}$.' +), ( 'SetxSet', 'skeletal', From 45aa96006b4637fe06ec3356b135d1cd6dcfb620 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 11:35:27 -0400 Subject: [PATCH 07/14] Resolve Barr-coexact for Top and Top* --- database/data/004_property-assignments/Top.sql | 6 ++++++ database/data/004_property-assignments/Top_pointed.sql | 9 ++++++--- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index 7b8cbdf8..3a694749 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/database/data/004_property-assignments/Top.sql @@ -118,4 +118,10 @@ VALUES 'coaccessible', FALSE, 'Assume $\mathbf{Top}$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\mathbf{Set}$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}$ is not coaccessible, this is a contradiction.' +), +( + 'Top', + 'Barr-coexact', + FALSE, + 'Consider the one-point space $X$, and $R$ is the corelation with two points and the indiscrete topology. Then for any space $Y$, the continuous functions $R \to Y$ correspond to the pairs of points which are indistinguishable in $Y$, which induces an equivalence relation on the pairs of maps $X \to Y$; this implies that $R$ is an equivalence corelation on $X$. However, the equalizer of the two maps $X \to R$ is empty, and the map $\emptyset \to X$ has cokernel pair given by the two-point discrete space.' ); diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index fa4e679d..034a2064 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -143,7 +143,10 @@ VALUES 'coaccessible', FALSE, 'We can adjust the proof for $\mathbf{Top}$ as follows: Assume $\mathbf{Top}_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\mathbf{Set}_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}_*$ is not coaccessible, this is a contradiction.' +), +( + 'Top*', + 'Barr-coexact', + FALSE, + 'Consider the two-point discrete space $X$, and $R$ is the corelation with three points $\{ *, a, b \}$ and topology $\{ \emptyset, \{ * \}, \{ a, b \}, \{ *, a, b \}$. Then for any space $Y$, the continuous functions $R \to Y$ correspond to the pairs of points which are indistinguishable in $Y$, which induces an equivalence relation on the pairs of maps $X \to Y$; this implies that $R$ is an equivalence corelation on $X$. However, the equalizer of the two maps $X \to R$ is just the base point, and the map $\{ * \} \to X$ has cokernel pair given by the three-point discrete space.' ); - - - From 6d3b14b3096e6b50042ff99c8229b881abd3c24e Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 11:55:46 -0400 Subject: [PATCH 08/14] Update expected properties --- scripts/expected-data/Ab.json | 6 +++++- scripts/expected-data/Set.json | 4 ++++ scripts/expected-data/Top.json | 6 +++++- 3 files changed, 14 insertions(+), 2 deletions(-) diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 97ebd8eb..48224d80 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -100,6 +100,9 @@ "multi-initial object": true, "cartesian filtered colimits": true, "cocartesian cofiltered limits": true, + "Barr-coexact": true, + "Barr-exact": true, + "monadically concrete": true, "cartesian closed": false, "locally cartesian closed": false, @@ -144,5 +147,6 @@ "essentially countable": false, "natural numbers object": false, "countably distributive": false, - "countably codistributive": false + "countably codistributive": false, + "pretopos": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 00206fe0..ac1d08f0 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -96,6 +96,10 @@ "cocartesian cofiltered limits": true, "natural numbers object": true, "countably distributive": true, + "Barr-coexact": true, + "Barr-exact": true, + "monadically concrete": true, + "pretopos": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0e6ea903..f9600169 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -144,5 +144,9 @@ "countable": false, "essentially countable": false, "cartesian filtered colimits": false, - "countably codistributive": false + "countably codistributive": false, + "Barr-coexact": false, + "Barr-exact": false, + "monadically concrete": false, + "pretopos": false } From 1baf45f03604af3f570d26f8e19331e7a8131e3e Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 12:27:04 -0400 Subject: [PATCH 09/14] Add monadically concrete -> cocomplete implication --- .../005_additional-structure-implications.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/005_implications/005_additional-structure-implications.sql b/database/data/005_implications/005_additional-structure-implications.sql index 2b475c9c..c056ac44 100644 --- a/database/data/005_implications/005_additional-structure-implications.sql +++ b/database/data/005_implications/005_additional-structure-implications.sql @@ -16,8 +16,8 @@ VALUES ( 'monadically_concrete_consequences', '["monadically concrete"]', - '["complete", "Barr-exact"]', - 'It is complete because a monadic functor creates limits. It is Barr-exact because any Eilenberg-Moore category of a functor on Set is Barr-exact.', + '["complete", "cocomplete", "Barr-exact"]', + 'It is complete because a monadic functor creates limits. For cocompleteness, see for example Handbook of Categorial Algebra Vol. 2, Thm. 4.3.5. For Barr-exactness, see here.', FALSE ), ( From 2701c0e90071579a5152d73f52b3bb8f8f625a9d Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 13:06:51 -0400 Subject: [PATCH 10/14] Add implication pretopos -> balanced --- .../005_implications/008_topos-theory-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index dcf9bd57..c7e2e3dd 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -48,6 +48,13 @@ VALUES 'By definition.', TRUE ), +( + 'pretopos_consequence', + '["pretopos"]', + '["balanced"]', + 'See NLab, Example 2.2 with a citation of Peter Johnstone, Cor. 1.22 in: Topos theory, London Math. Soc. Monographs 10, Acad. Press (1977), Dover (2014).', + FALSE +), ( 'topos_definition', '["elementary topos"]', From beff588fb9c55ad3eae34622de695ec206869ecf Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 14:34:28 -0400 Subject: [PATCH 11/14] Add some related properties, and a bit of background on the relevance of regularity to Barr-exactness --- .../003_properties/003_limits-colimits-behavior.sql | 4 ++-- .../data/003_properties/100_related-properties.sql | 10 ++++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 89d89979..7a825a8e 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -199,7 +199,7 @@ VALUES ( 'Barr-exact', 'is', - 'A category is Barr-exact if it is regular, and in addition, every internal equivalence relation is a kernel pair.', + 'A category is Barr-exact if it is regular, and in addition, every internal equivalence relation is a kernel pair. (Note that because of the regularity condition, that is equivalent to being the kernel pair of a coequalizer of the two projections.)', 'https://ncatlab.org/nlab/show/exact', 'Barr-coexact', TRUE @@ -207,7 +207,7 @@ VALUES ( 'Barr-coexact', 'is', - 'A category is Barr-coexact if its dual is Barr-exact, i.e. it is coregular, and in addition, every internal equivalence corelation is a cokernel pair.', + 'A category is Barr-coexact if its dual is Barr-exact, i.e. it is coregular, and in addition, every internal equivalence corelation is a cokernel pair. (Note that because of the coregularity condition, that is equivalent to being the cokernel pair of an equalizer of the two coprojections.)', NULL, 'Barr-exact', TRUE diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index dfd1b997..c69145e5 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -60,7 +60,13 @@ VALUES ('elementary topos', 'finitely complete'), ('elementary topos', 'subobject classifier'), ('elementary topos', 'natural numbers object'), +('elementary topos', 'pretopos'), ('Grothendieck topos', 'elementary topos'), +('Grothendieck topos', 'pretopos'), +('pretopos', 'extensive'), +('pretopos', 'Barr-exact'), +('pretopos', 'elementary topos'), +('pretopos', 'Grothendieck topos'), ('natural numbers object', 'elementary topos'), ('natural numbers object', 'finite products'), ('initial object', 'finite coproducts'), @@ -229,6 +235,10 @@ VALUES ('strongly connected', 'inhabited'), ('regular', 'finitely complete'), ('coregular', 'finitely cocomplete'), +('Barr-exact', 'regular'), +('Barr-exact', 'coequalizers'), +('Barr-coexact', 'coregular'), +('Barr-coexact', 'equalizers'), ('extensive', 'infinitary extensive'), ('extensive', 'finite coproducts'), ('extensive', 'disjoint finite coproducts'), From 856f2e6248d063b6a92841e18853e7dca299365d Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 14:55:57 -0400 Subject: [PATCH 12/14] Add local essential smallness consequence of monadically concrete --- .../005_additional-structure-implications.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/005_implications/005_additional-structure-implications.sql b/database/data/005_implications/005_additional-structure-implications.sql index c056ac44..f65b08cf 100644 --- a/database/data/005_implications/005_additional-structure-implications.sql +++ b/database/data/005_implications/005_additional-structure-implications.sql @@ -16,8 +16,8 @@ VALUES ( 'monadically_concrete_consequences', '["monadically concrete"]', - '["complete", "cocomplete", "Barr-exact"]', - 'It is complete because a monadic functor creates limits. For cocompleteness, see for example Handbook of Categorial Algebra Vol. 2, Thm. 4.3.5. For Barr-exactness, see here.', + '["complete", "cocomplete", "Barr-exact", "locally essentially small"]', + 'It is complete because a monadic functor creates limits. For cocompleteness, see for example Handbook of Categorial Algebra Vol. 2, Thm. 4.3.5. For Barr-exactness, see here. The local smallness condition is easy from the fact that the monadic functor must be faithful.', FALSE ), ( From 2b089db3c3bb2bcc5f27c28b333dd3d9dba435e8 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 15:36:18 -0400 Subject: [PATCH 13/14] Add not Barr-coexact data for Prost --- database/data/004_property-assignments/Prost.sql | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/database/data/004_property-assignments/Prost.sql b/database/data/004_property-assignments/Prost.sql index 3b0a67b5..91411889 100644 --- a/database/data/004_property-assignments/Prost.sql +++ b/database/data/004_property-assignments/Prost.sql @@ -94,4 +94,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509552: Consider the forgetful functor $U : \mathbf{Prost} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' +), +( + 'Prost', + 'Barr-coexact', + FALSE, + 'Consider the space $X$ with one point, and the corelation $R$ with two points and the full relation. Then for any $Y$, the morphisms $R \to Y$ correspond to pairs of points $(y_1, y_2) \in Y \times Y$ such that $y_1 \le y_2$ and $y_2 \le y_1$, which induces an equivalence relation on pairs of maps $X \to Y$. It follows that $R$ is an equivalence corelation. However, the equalizer of the two maps $X \to R$ is empty, and the cokernel pair of the map $\emptyset \to X$ is the proset with two elements and the equality relation.' ); From 1126ed3874742e6f0ddd966b0455e2cf15e9964a Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 18 Apr 2026 19:50:58 -0400 Subject: [PATCH 14/14] Fix garbled language around kernel pairs in some of the proofs --- database/data/004_property-assignments/FinSet.sql | 2 +- database/data/004_property-assignments/FreeAb.sql | 2 +- database/data/004_property-assignments/Haus.sql | 2 +- database/data/004_property-assignments/Met_c.sql | 2 +- database/data/004_property-assignments/Met_oo.sql | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index 885bcb01..9c3f5c2c 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/database/data/004_property-assignments/FinSet.sql @@ -51,7 +51,7 @@ VALUES 'FinSet', 'Barr-coexact', TRUE, - 'If an equivalence corelation is a cokernel pair of $f, g : Y \to X$, then we can replace $Y$ with the appropriate equalizer which is finite.' + 'If an equivalence corelation is a cokernel pair of $f : Y \to X$ where $Y$ is gotten from Barr-coexactness of $\mathbf{Set}$, then we can replace $Y$ with the appropriate equalizer which is finite.' ), ( 'FinSet', diff --git a/database/data/004_property-assignments/FreeAb.sql b/database/data/004_property-assignments/FreeAb.sql index 007a0db5..f4fb9989 100644 --- a/database/data/004_property-assignments/FreeAb.sql +++ b/database/data/004_property-assignments/FreeAb.sql @@ -89,5 +89,5 @@ VALUES 'FreeAb', 'Barr-exact', FALSE, - 'Any kernel pair $E$ of a pair of morphisms to a free Abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$. However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.' + 'Any kernel pair $E$ of a morphism to a free Abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$. However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.' ); diff --git a/database/data/004_property-assignments/Haus.sql b/database/data/004_property-assignments/Haus.sql index 798fbc7d..1ceafe0e 100644 --- a/database/data/004_property-assignments/Haus.sql +++ b/database/data/004_property-assignments/Haus.sql @@ -99,6 +99,6 @@ VALUES 'Haus', 'Barr-exact', FALSE, - 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' + 'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' ); diff --git a/database/data/004_property-assignments/Met_c.sql b/database/data/004_property-assignments/Met_c.sql index e6cdd216..e76f3f9d 100644 --- a/database/data/004_property-assignments/Met_c.sql +++ b/database/data/004_property-assignments/Met_c.sql @@ -105,5 +105,5 @@ VALUES 'Met_c', 'Barr-exact', FALSE, - 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' + 'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' ); diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index 1f0ad8d6..632f727b 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/database/data/004_property-assignments/Met_oo.sql @@ -87,5 +87,5 @@ VALUES 'Met_oo', 'Barr-exact', FALSE, - 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' + 'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' );