Add "countable" and "essentially countable"

Author: ykawase5048

database/data/003_properties/004_size-constraints.sql

@@ -63,6 +63,22 @@ VALUES
 	'essentially finite',
 	TRUE
 ),
+(
+	'countable',
+	'is',
+	'A category is <i>countable</i> if it has countably many objects and morphisms.',
+	NULL,
+	'countable',
+	FALSE
+),
+(
+	'essentially countable',
+	'is',
+	'A category is <i>essentially countable</i> if it is equivalent to a countable category.',
+	NULL,
+	'essentially countable',
+	TRUE
+),
 (
 	'well-powered',
 	'is',

database/data/005_implications/003_size-constraints-implications.sql

@@ -23,13 +23,27 @@ VALUES
 (
 	'finite_consequence',
 	'["finite"]',
-	'["small", "essentially finite"]',
+	'["countable", "essentially finite"]',
 	'This is trivial.',
 	FALSE
 ),
 (
-	'essentially_finite_consequence',
+	'essentially_finite_raise',
 	'["essentially finite"]',
+	'["essentially countable"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'countable_consequence',
+	'["countable"]',
+	'["essentially countable"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'essentially_countable_consequence',
+	'["essentially countable"]',
 	'["essentially small"]',
 	'This is trivial.',
 	FALSE

database/data/005_implications/007_locally-presentable-implications.sql

@@ -125,6 +125,13 @@ VALUES
 	'See <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Thm. 2.2.2.',
 	TRUE
 ),
+(
+	'countably_accessible_thin',
+	'["essentially countable", "thin"]',
+	'["ℵ₁-accessible"]',
+	'In general, every $\kappa$-filtered diagram in a poset whose elements are less than $\kappa$ admits the greatest element. Therefore, all the elements are $\kappa$-presentable, and the poset is $\kappa$-accessible.',
+	FALSE
+),
 (
 	'locally_presentable_another_definition',
 	'["locally presentable"]',