Skip to content

Add "locally cartesian closed" property #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ScriptRaccoon merged 1 commit into from
Mar 22, 2026
+183 −12
Merged

Add "locally cartesian closed" property #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions database/data/001_categories.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
(
Expand Down
3 changes: 3 additions & 0 deletions database/data/002_tags.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'),
Expand Down
1 change: 1 addition & 0 deletions database/data/003_related-categories.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'),
Expand Down
16 changes: 16 additions & 0 deletions database/data/005_properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,14 @@ VALUES
NULL,
TRUE
),
(
'locally cartesian closed',
'is',
'A category is <i>locally cartesian closed</i> if each of its slice categories is cartesian closed.',
'https://ncatlab.org/nlab/show/locally+cartesian+closed+category',
NULL,
TRUE
),
(
'pullbacks',
'has',
Expand Down Expand Up @@ -581,6 +589,14 @@ VALUES
'connected',
TRUE
),
(
'strongly connected',
'is',
'A category is <i>strongly connected</i> 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',
Expand Down
5 changes: 4 additions & 1 deletion database/data/006_related_properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'),
Expand Down Expand Up @@ -85,4 +86,6 @@ VALUES
('wide pushouts', 'pushouts'),
('split abelian', 'abelian'),
('Cauchy complete', 'finitely complete'),
('Malcev', 'finitely complete');
('Malcev', 'finitely complete'),
('connected', 'strongly connected'),
('strongly connected', 'connected');
90 changes: 82 additions & 8 deletions database/data/007_category-satisfied-properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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',
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -631,6 +651,11 @@ VALUES
'finite',
'trivial'
),
(
'0',
'locally cartesian closed',
'This is vacuously true.'
),
(
'1',
'trivial',
Expand Down Expand Up @@ -686,7 +711,11 @@ VALUES
'skeletal',
'The two objects are not isomorphic'
),

(
'walking_morphism',
'strongly connected',
'trivial'
),
(
'walking_pair',
'finite',
Expand All @@ -699,7 +728,7 @@ VALUES
),
(
'walking_pair',
'connected',
'strongly connected',
'trivial'
),
(
Expand Down Expand Up @@ -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
(
Expand Down Expand Up @@ -1072,6 +1126,11 @@ VALUES
'skeletal',
'The relation $\leq$ is antisymmetric.'
),
(
'N',
'strongly connected',
'trivial'
),
(
'On',
'thin',
Expand Down Expand Up @@ -1107,6 +1166,11 @@ VALUES
'skeletal',
'The relation $\leq$ is antisymmetric'
),
(
'On',
'strongly connected',
'trivial'
),
(
'real_interval',
'small',
Expand All @@ -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',
Expand Down Expand Up @@ -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
(
Expand All @@ -1201,7 +1270,7 @@ VALUES
),
(
'BG',
'connected',
'strongly connected',
'trivial'
),
(
Expand All @@ -1226,7 +1295,7 @@ VALUES
),
(
'BGf',
'connected',
'strongly connected',
'trivial'
),
(
Expand All @@ -1246,7 +1315,7 @@ VALUES
),
(
'BN',
'connected',
'strongly connected',
'trivial'
),
(
Expand Down Expand Up @@ -1277,7 +1346,7 @@ VALUES

(
'BOn',
'connected',
'strongly connected',
'trivial'
),
(
Expand Down Expand Up @@ -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',
Expand Down
10 changes: 10 additions & 0 deletions database/data/008_category-unsatisfied-properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <a href="http://www.tac.mta.ca/tac/volumes/8/n2/8-02abs.html" target="_blank">Niefield 2001</a>.'
),
(
'M-Set',
'strict terminal object',
Expand Down Expand Up @@ -1131,6 +1136,11 @@ VALUES
'Malcev',
NULL
),
(
'Cat',
'locally cartesian closed',
'See Theorem 4.4 of <a href="https://www.numdam.org/item/MSMF_1964__2__R3_0/" target="_blank">Giraud 1964</a>.'
),
(
'Fld',
'connected',
Expand Down
Loading