diff --git a/database/data/001_categories.sql b/database/data/001_categories.sql
index 1a524597..29896502 100644
--- a/database/data/001_categories.sql
+++ b/database/data/001_categories.sql
@@ -284,6 +284,15 @@ VALUES
'The name of this category comes from the fact that it consists of two objects and an isomorphism between them, and a functor out of this category is the same as an isomorphism in the target category. The walking isomorphism is actually equivalent to the trivial category.',
'https://ncatlab.org/nlab/show/walking+isomorphism'
),
+ (
+ 'walking_composable_pair',
+ 'walking composable pair',
+ '$\{ 0 \to 1 \to 2 \}$',
+ 'three objects $0,1,2$',
+ 'a single morphism from each natural number to one greater than or equal to it',
+ 'The name of this category comes from the fact that a functor out of it is the same as a composable pair of morphisms.',
+ 'https://ncatlab.org/nlab/show/composable+pair'
+ ),
-- examples of thin categories
(
diff --git a/database/data/002_tags.sql b/database/data/002_tags.sql
index 7939de64..97cd2cec 100644
--- a/database/data/002_tags.sql
+++ b/database/data/002_tags.sql
@@ -161,6 +161,9 @@ VALUES
('walking_isomorphism', 'artificial'),
('walking_isomorphism', 'category theory'),
('walking_isomorphism', 'badly-behaved'),
+ ('walking_composable_pair', 'artificial'),
+ ('walking_composable_pair', 'category theory'),
+ ('walking_composable_pair', 'badly-behaved'),
('Setne', 'artificial'),
('Setne', 'set theory'),
('Setne', 'well-behaved'),
diff --git a/database/data/003_related-categories.sql b/database/data/003_related-categories.sql
index 97a400c5..ddbb8bfd 100644
--- a/database/data/003_related-categories.sql
+++ b/database/data/003_related-categories.sql
@@ -80,6 +80,7 @@ VALUES
('walking_pair', 'walking_morphism'),
('walking_isomorphism', 'walking_morphism'),
('walking_isomorphism', '1'),
+ ('walking_composable_pair', 'walking_morphism'),
('Setne', 'Set'),
('B', 'FI'),
('B', 'FS'),
diff --git a/database/data/005_properties.sql b/database/data/005_properties.sql
index 8eb0d487..a414a90f 100644
--- a/database/data/005_properties.sql
+++ b/database/data/005_properties.sql
@@ -32,6 +32,14 @@ VALUES
NULL,
TRUE
),
+ (
+ 'locally cartesian closed',
+ 'is',
+ 'A category is locally cartesian closed if each of its slice categories is cartesian closed.',
+ 'https://ncatlab.org/nlab/show/locally+cartesian+closed+category',
+ NULL,
+ TRUE
+ ),
(
'pullbacks',
'has',
@@ -581,6 +589,14 @@ VALUES
'connected',
TRUE
),
+ (
+ 'strongly connected',
+ 'is',
+ 'A category is strongly connected if it is inhabited and every two objects $A,B$ can be joined via a morphism: there is a morphism $A \to B$ or there is a morphism $B \to A$. Notice that this is stronger than being connected, and that posets with this property are precisely the inhabited totally ordered sets.',
+ NULL,
+ 'strongly connected',
+ TRUE
+ ),
(
'balanced',
'is',
diff --git a/database/data/006_related_properties.sql b/database/data/006_related_properties.sql
index e3189899..42757b1c 100644
--- a/database/data/006_related_properties.sql
+++ b/database/data/006_related_properties.sql
@@ -4,6 +4,7 @@ VALUES
('locally small', 'locally essentially small'),
('locally essentially small', 'locally small'),
('cartesian closed', 'finite products'),
+ ('locally cartesian closed', 'cartesian closed'),
('zero morphisms', 'preadditive'),
('zero morphisms', 'pointed'),
('preadditive', 'additive'),
@@ -85,4 +86,6 @@ VALUES
('wide pushouts', 'pushouts'),
('split abelian', 'abelian'),
('Cauchy complete', 'finitely complete'),
- ('Malcev', 'finitely complete');
\ No newline at end of file
+ ('Malcev', 'finitely complete'),
+ ('connected', 'strongly connected'),
+ ('strongly connected', 'connected');
\ No newline at end of file
diff --git a/database/data/007_category-satisfied-properties.sql b/database/data/007_category-satisfied-properties.sql
index e236a83d..d2276661 100644
--- a/database/data/007_category-satisfied-properties.sql
+++ b/database/data/007_category-satisfied-properties.sql
@@ -21,6 +21,11 @@ VALUES
'Grothendieck topos',
'It is equivalent to the category of sheaves on a one-point space.'
),
+ (
+ 'Set',
+ 'strongly connected',
+ 'Every nonempty set is weakly terminal.'
+ ),
(
'Set',
'finitary algebraic',
@@ -86,6 +91,11 @@ VALUES
'disjoint coproducts',
'This follows easily from the corresponding fact for sets.'
),
+ (
+ 'Top',
+ 'strongly connected',
+ 'Every nonempty space is weakly terminal.'
+ ),
(
'Grp',
'locally small',
@@ -356,6 +366,11 @@ VALUES
'disjoint coproducts',
'This follows easily from the corresponding fact for sets, since the coproduct of posets is built using the disjoint union.'
),
+ (
+ 'Pos',
+ 'strongly connected',
+ 'Every nonempty preorder is weakly terminal.'
+ ),
(
'M-Set',
'locally small',
@@ -463,6 +478,11 @@ VALUES
'generator',
'The one-point set is a generator since it represents the forgetful functor $\mathbf{FinSet} \to \mathbf{Set}$.'
),
+ (
+ 'FinSet',
+ 'strongly connected',
+ 'Every nonempty finite set is weakly terminal.'
+ ),
(
'FinSet',
'cogenerator',
@@ -631,6 +651,11 @@ VALUES
'finite',
'trivial'
),
+ (
+ '0',
+ 'locally cartesian closed',
+ 'This is vacuously true.'
+ ),
(
'1',
'trivial',
@@ -686,7 +711,11 @@ VALUES
'skeletal',
'The two objects are not isomorphic'
),
-
+ (
+ 'walking_morphism',
+ 'strongly connected',
+ 'trivial'
+ ),
(
'walking_pair',
'finite',
@@ -699,7 +728,7 @@ VALUES
),
(
'walking_pair',
- 'connected',
+ 'strongly connected',
'trivial'
),
(
@@ -732,6 +761,31 @@ VALUES
'finite',
'trivial'
),
+ (
+ 'walking_composable_pair',
+ 'finite',
+ 'trivial'
+ ),
+ (
+ 'walking_composable_pair',
+ 'strongly connected',
+ 'trivial'
+ ),
+ (
+ 'walking_composable_pair',
+ 'skeletal',
+ 'trivial'
+ ),
+ (
+ 'walking_composable_pair',
+ 'products',
+ 'trivial'
+ ),
+ (
+ 'walking_composable_pair',
+ 'self-dual',
+ 'trivial'
+ ),
-- geometric categories
(
@@ -1072,6 +1126,11 @@ VALUES
'skeletal',
'The relation $\leq$ is antisymmetric.'
),
+ (
+ 'N',
+ 'strongly connected',
+ 'trivial'
+ ),
(
'On',
'thin',
@@ -1107,6 +1166,11 @@ VALUES
'skeletal',
'The relation $\leq$ is antisymmetric'
),
+ (
+ 'On',
+ 'strongly connected',
+ 'trivial'
+ ),
(
'real_interval',
'small',
@@ -1119,8 +1183,8 @@ VALUES
),
(
'real_interval',
- 'cartesian closed',
- 'The exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.'
+ 'strongly connected',
+ 'trivial'
),
(
'real_interval',
@@ -1187,6 +1251,11 @@ VALUES
'infinitary codistributive',
'We need to prove $\max(a, \inf_i b_i) = \inf_i \max(a,b_i)$. The inequality $\leq$ is formal, we need to prove $\geq$. For the empty index set both sides are $\infty$. Otherwise, there is some $i_0$ with $b_{i_0} = \inf_i b_i$. Then $\max(a, \inf_i b_i) = \max(a, b_{i_0}) \geq \inf_i \max(a,b_i)$.'
),
+ (
+ 'Noo',
+ 'strongly connected',
+ 'trivial'
+ ),
-- deloopings
(
@@ -1201,7 +1270,7 @@ VALUES
),
(
'BG',
- 'connected',
+ 'strongly connected',
'trivial'
),
(
@@ -1226,7 +1295,7 @@ VALUES
),
(
'BGf',
- 'connected',
+ 'strongly connected',
'trivial'
),
(
@@ -1246,7 +1315,7 @@ VALUES
),
(
'BN',
- 'connected',
+ 'strongly connected',
'trivial'
),
(
@@ -1277,7 +1346,7 @@ VALUES
(
'BOn',
- 'connected',
+ 'strongly connected',
'trivial'
),
(
@@ -1412,6 +1481,11 @@ VALUES
'disjoint coproducts',
'This follows easily from the description of a coproduct of categories (based on disjoint unions).'
),
+ (
+ 'Cat',
+ 'strongly connected',
+ 'Every nonempty category is weakly terminal.'
+ ),
(
'Fld',
'locally small',
diff --git a/database/data/008_category-unsatisfied-properties.sql b/database/data/008_category-unsatisfied-properties.sql
index e1a7001b..0807b606 100644
--- a/database/data/008_category-unsatisfied-properties.sql
+++ b/database/data/008_category-unsatisfied-properties.sql
@@ -311,6 +311,11 @@ VALUES
'Malcev',
'Consider the subposet $\{(a,b) : a \leq b \}$ of $\mathbb{N}^2$.'
),
+ (
+ 'Pos',
+ 'locally cartesian closed',
+ 'See ยง2 of Niefield 2001.'
+ ),
(
'M-Set',
'strict terminal object',
@@ -1131,6 +1136,11 @@ VALUES
'Malcev',
NULL
),
+ (
+ 'Cat',
+ 'locally cartesian closed',
+ 'See Theorem 4.4 of Giraud 1964.'
+ ),
(
'Fld',
'connected',
diff --git a/database/data/010_implications.sql b/database/data/010_implications.sql
index b3ce907f..603e54aa 100644
--- a/database/data/010_implications.sql
+++ b/database/data/010_implications.sql
@@ -278,10 +278,10 @@ VALUES
FALSE
),
(
- 'connected_criterion',
+ 'zero_morphisms_mean_strongly_connected',
'["zero morphisms", "inhabited"]',
- '["connected"]',
- 'This is trivial.',
+ '["strongly connected"]',
+ 'This holds by definition.',
FALSE
),
(
@@ -403,6 +403,13 @@ VALUES
'This is easy.',
FALSE
),
+ (
+ 'groupoid_connected',
+ '["groupoid", "connected"]',
+ '["strongly connected"]',
+ 'trivial',
+ FALSE
+ ),
(
'connected_consequence',
'["connected"]',
@@ -410,6 +417,13 @@ VALUES
'This holds by definition.',
FALSE
),
+ (
+ 'strongly_connected_consequence',
+ '["strongly connected"]',
+ '["connected"]',
+ 'This holds by definition.',
+ FALSE
+ ),
(
'generator_consequence',
'["generator"]',
@@ -643,6 +657,34 @@ VALUES
'See Prop. 2.2.13. in Malcev, protomodular, homological and semi-abelian categories.',
FALSE
),
+ (
+ 'pullbacks_are_local_products',
+ '["locally cartesian closed"]',
+ '["pullbacks"]',
+ 'Pullbacks are binary products in slice categories.',
+ FALSE
+ ),
+ (
+ 'locally_cartesian_closed_with_terminal_is_closed',
+ '["locally cartesian closed", "terminal object"]',
+ '["cartesian closed"]',
+ 'The slice over the terminal object is the category itself.',
+ FALSE
+ ),
+ (
+ 'discrete_is_locally_cartesian_closed',
+ '["discrete"]',
+ '["locally cartesian closed"]',
+ 'Each slice of a discrete category is terminal.',
+ FALSE
+ ),
+ (
+ 'sequential_implies_lcc',
+ '["thin", "strongly connected"]',
+ '["locally cartesian closed"]',
+ 'Each slice is thin, strongly connected, and has a terminal object. Every such category is cartesian closed, where the exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.',
+ FALSE
+ ),
-- non-trivial implications
(
@@ -721,5 +763,12 @@ 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
+ ),
+ (
+ 'topos_is_locally_cartesian_closed',
+ '["elementary topos"]',
+ '["locally cartesian closed"]',
+ 'See Johnstone, Cor. A2.3.4.',
+ FALSE
);
diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json
index 67d8dd17..0685fb75 100644
--- a/scripts/expected-data/Ab.json
+++ b/scripts/expected-data/Ab.json
@@ -10,6 +10,7 @@
"cogenerator": true,
"complete": true,
"connected": true,
+ "strongly connected": true,
"connected colimits": true,
"connected limits": true,
"coproducts": true,
@@ -56,6 +57,7 @@
"biproducts": true,
"cartesian closed": false,
+ "locally cartesian closed": false,
"discrete": false,
"distributive": false,
"elementary topos": false,
diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json
index 2c382a71..248fab8a 100644
--- a/scripts/expected-data/Set.json
+++ b/scripts/expected-data/Set.json
@@ -5,11 +5,13 @@
"binary coproducts": true,
"binary products": true,
"cartesian closed": true,
+ "locally cartesian closed": true,
"cocomplete": true,
"coequalizers": true,
"cogenerator": true,
"complete": true,
"connected": true,
+ "strongly connected": true,
"connected colimits": true,
"connected limits": true,
"coproducts": true,
diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json
index 44390a6d..1fa7baf9 100644
--- a/scripts/expected-data/Top.json
+++ b/scripts/expected-data/Top.json
@@ -7,6 +7,7 @@
"cogenerator": true,
"complete": true,
"connected": true,
+ "strongly connected": true,
"connected colimits": true,
"connected limits": true,
"coproducts": true,
@@ -46,6 +47,7 @@
"additive": false,
"balanced": false,
"cartesian closed": false,
+ "locally cartesian closed": false,
"discrete": false,
"elementary topos": false,
"epi-regular": false,