ScriptRaccoon · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026 · Oct 27, 2026
diff --git a/.cspell.json b/.cspell.json
@@ -165,6 +165,7 @@
 		"cospans",
 		"cosymmetric",
 		"cosymmetry",
+		"cotopos",
 		"cototal",
 		"cotransitive",
 		"cotransitivity",
@@ -327,6 +328,7 @@
 		"precomposed",
 		"precomposing",
 		"precomposition",
+		"precotopos",
 		"preimage",
 		"preimages",
 		"preorder",
@@ -348,6 +350,7 @@
 		"pushforward",
 		"pushout",
 		"pushouts",
+		"quasicotopos",
 		"quasitopos",
 		"Quillan",
 		"Reggio",

diff --git a/database/data/category-properties/Barr-coexact.yaml b/database/data/category-properties/Barr-coexact.yaml
@@ -9,6 +9,7 @@ related:
   - coregular
   - effective cocongruences
   - coquotients of cocongruences
+  - precotopos
 
 tags:
   - limit–colimit interaction

diff --git a/database/data/category-properties/Grothendieck cotopos.yaml b/database/data/category-properties/Grothendieck cotopos.yaml
@@ -0,0 +1,12 @@
+id: Grothendieck cotopos
+relation: is a
+description: A <i>Grothendieck cotopos</i> is a category whose opposite is a Grothendieck topos.
+nlab_link: https://ncatlab.org/nlab/show/cotopos
+dual: Grothendieck topos
+invariant_under_equivalences: true
+
+related:
+  - elementary cotopos
+
+tags:
+  - topos theory
diff --git a/database/data/category-properties/Grothendieck topos.yaml b/database/data/category-properties/Grothendieck topos.yaml
@@ -2,7 +2,7 @@ id: Grothendieck topos
 relation: is a
 description: A <i>Grothendieck topos</i> is a category that is equivalent to the category of sheaves on a site.
 nlab_link: https://ncatlab.org/nlab/show/Grothendieck+topos
-dual: null
+dual: Grothendieck cotopos
 invariant_under_equivalences: true
 
 related:

diff --git a/database/data/category-properties/coextensive.yaml b/database/data/category-properties/coextensive.yaml
@@ -10,6 +10,7 @@ related:
   - codistributive
   - infinitary coextensive
   - countably coextensive
+  - precotopos
 
 tags:
   - limit–colimit interaction
diff --git a/database/data/category-properties/elementary cotopos.yaml b/database/data/category-properties/elementary cotopos.yaml
@@ -0,0 +1,17 @@
+id: elementary cotopos
+relation: is an
+description: An <i>elementary cotopos</i> is a category whose dual category is an elementary topos, i.e. a cocartesian coclosed category with finite colimits and a quotient object classifier.
+nlab_link: https://ncatlab.org/nlab/show/cotopos
+dual: elementary topos
+invariant_under_equivalences: true
+
+related:
+  - cocartesian coclosed
+  - finitely cocomplete
+  - quotient object classifier
+  - Grothendieck cotopos
+  - precotopos
+  - quasitopos
+
+tags:
+  - topos theory
diff --git a/database/data/category-properties/elementary topos.yaml b/database/data/category-properties/elementary topos.yaml
@@ -2,17 +2,17 @@ id: elementary topos
 relation: is an
 description: An <i>elementary topos</i> is a cartesian closed category with finite limits and a subobject classifier.
 nlab_link: https://ncatlab.org/nlab/show/topos
-dual: null
+dual: elementary cotopos
 invariant_under_equivalences: true
 
 related:
-  - Grothendieck topos
   - cartesian closed
   - finitely complete
-  - parametrized natural numbers object
   - subobject classifier
+  - Grothendieck topos
   - pretopos
   - quasitopos
+  - parametrized natural numbers object
 
 tags:
   - topos theory
diff --git a/database/data/category-properties/precotopos.yaml b/database/data/category-properties/precotopos.yaml
@@ -0,0 +1,16 @@
+id: precotopos
+relation: is a
+description: A <i>precotopos</i> is a category whose opposite is a pretopos. Equivalently, it is Barr-coexact and coextensive. This terminology is not standard.
+nlab_link: null
+dual: pretopos
+invariant_under_equivalences: true
+
+related:
+  - Barr-coexact
+  - coextensive
+  - elementary cotopos
+  - epi-regular
+
+tags:
+  - topos theory
+  - limit–colimit interaction
diff --git a/database/data/category-properties/pretopos.yaml b/database/data/category-properties/pretopos.yaml
@@ -2,7 +2,7 @@ id: pretopos
 relation: is a
 description: A <i>pretopos</i> is a category which is Barr-exact and extensive.
 nlab_link: https://ncatlab.org/nlab/show/pretopos
-dual: null
+dual: precotopos
 invariant_under_equivalences: true
 
 related:

diff --git a/database/data/category-properties/quasicotopos.yaml b/database/data/category-properties/quasicotopos.yaml
@@ -0,0 +1,20 @@
+id: quasicotopos
+relation: is a
+description: >-
+  A <i>quasicotopos</i> is a category whose opposite is a quasitopos. This means that it is finitely complete, finitely cocomplete, locally cocartesian coclosed, and has a regular quotient object classifier. This terminology is not standard.
+nlab_link: null
+dual: quasitopos
+invariant_under_equivalences: true
+
+keywords:
+  - quasi-cotopos
+
+related:
+  - finitely complete
+  - finitely cocomplete
+  - locally cocartesian coclosed
+  - regular quotient object classifier
+  - elementary cotopos
+
+tags:
+  - topos theory
diff --git a/database/data/category-properties/quasitopos.yaml b/database/data/category-properties/quasitopos.yaml
@@ -5,7 +5,7 @@ description: >-
 
   Note that some authors use a strong subobject classifier in place of a regular subobject classifier in the definition, i.e. a morphism $\top : 1 \to \Omega$ which classifies strong monomorphisms. For the equivalence of these definitions, see <a href="https://math.stackexchange.com/q/4335533">MSE/4335533</a>.
 nlab_link: https://ncatlab.org/nlab/show/quasitopos
-dual: null
+dual: quasicotopos
 invariant_under_equivalences: true
 
 keywords:

diff --git a/database/data/category-properties/quotient object classifier.yaml b/database/data/category-properties/quotient object classifier.yaml
@@ -5,13 +5,14 @@ description: >-
   $$\begin{CD} \Psi @>{\top}>> 0 \\ @V{\psi_e}VV @VV{!}V \\ A @>>{e}> B \end{CD}$$
   is a pushout diagram. Equivalently, the functor $\Quot : \C \to \Set^+$ is representable.
   *Every morphism $\Psi \to 0$ is a split epimorphism anyway.
-nlab_link: null
+nlab_link: https://ncatlab.org/nlab/show/quotient+object+coclassifier
 dual: subobject classifier
 invariant_under_equivalences: true
 
 related:
   - finitely cocomplete
   - regular quotient object classifier
+  - elementary cotopos
 
 tags:
   - topos theory

diff --git a/database/data/category-properties/regular quotient object classifier.yaml b/database/data/category-properties/regular quotient object classifier.yaml
@@ -12,6 +12,7 @@ invariant_under_equivalences: true
 related:
   - finitely cocomplete
   - quotient object classifier
+  - quasicotopos
 
 tags:
   - topos theory

diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json
@@ -150,6 +150,7 @@
 		"direct",
 		"discrete",
 		"distributive",
+		"elementary cotopos",
 		"elementary topos",
 		"essentially countable",
 		"essentially discrete",
@@ -160,6 +161,7 @@
 		"finite",
 		"finitely coaccessible",
 		"gaunt",
+		"Grothendieck cotopos",
 		"Grothendieck topos",
 		"groupoid",
 		"infinitary codistributive",
@@ -176,7 +178,9 @@
 		"locally ℵ₁-copresentable",
 		"one-way",
 		"parametrized natural numbers object",
+		"precotopos",
 		"pretopos",
+		"quasicotopos",
 		"quasitopos",
 		"quotient object classifier",
 		"quotient-trivial",

diff --git a/database/scripts/expected-data/FinSet.json b/database/scripts/expected-data/FinSet.json
@@ -124,6 +124,7 @@
 		"disjoint coproducts",
 		"disjoint finite products",
 		"disjoint products",
+		"elementary cotopos",
 		"essentially discrete",
 		"essentially finite",
 		"exact cofiltered limits",
@@ -137,6 +138,7 @@
 		"gaunt",
 		"generalized variety",
 		"Grothendieck abelian",
+		"Grothendieck cotopos",
 		"Grothendieck topos",
 		"groupoid",
 		"infinitary codistributive",
@@ -168,7 +170,9 @@
 		"pointed",
 		"powers",
 		"preadditive",
+		"precotopos",
 		"products",
+		"quasicotopos",
 		"quotient object classifier",
 		"quotient-trivial",
 		"regular quotient object classifier",

diff --git a/database/scripts/expected-data/N.json b/database/scripts/expected-data/N.json
@@ -126,6 +126,7 @@
 		"disjoint finite products",
 		"disjoint products",
 		"distributive",
+		"elementary cotopos",
 		"elementary topos",
 		"epi-regular",
 		"essentially discrete",
@@ -144,6 +145,7 @@
 		"finitely complete",
 		"generalized variety",
 		"Grothendieck abelian",
+		"Grothendieck cotopos",
 		"Grothendieck topos",
 		"groupoid",
 		"infinitary codistributive",
@@ -171,8 +173,10 @@
 		"pointed",
 		"powers",
 		"preadditive",
+		"precotopos",
 		"pretopos",
 		"products",
+		"quasicotopos",
 		"quasitopos",
 		"quotient object classifier",
 		"quotient-trivial",

diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json
@@ -153,6 +153,7 @@
 		"discrete",
 		"disjoint finite products",
 		"disjoint products",
+		"elementary cotopos",
 		"essentially countable",
 		"essentially discrete",
 		"essentially finite",
@@ -162,6 +163,7 @@
 		"finitely coaccessible",
 		"gaunt",
 		"Grothendieck abelian",
+		"Grothendieck cotopos",
 		"groupoid",
 		"infinitary codistributive",
 		"infinitary coextensive",
@@ -178,6 +180,8 @@
 		"one-way",
 		"pointed",
 		"preadditive",
+		"precotopos",
+		"quasicotopos",
 		"quotient object classifier",
 		"quotient-trivial",
 		"regular quotient object classifier",

diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json
@@ -128,6 +128,7 @@
 		"disjoint products",
 		"effective cocongruences",
 		"effective congruences",
+		"elementary cotopos",
 		"elementary topos",
 		"epi-regular",
 		"essentially countable",
@@ -145,6 +146,7 @@
 		"gaunt",
 		"generalized variety",
 		"Grothendieck abelian",
+		"Grothendieck cotopos",
 		"Grothendieck topos",
 		"groupoid",
 		"infinitary codistributive",
@@ -172,8 +174,10 @@
 		"one-way",
 		"pointed",
 		"preadditive",
+		"precotopos",
 		"pretopos",
 		"pullback-stable regular epimorphisms",
+		"quasicotopos",
 		"quasitopos",
 		"quotient object classifier",
 		"quotient-trivial",

diff --git a/database/scripts/expected-data/walking_morphism.json b/database/scripts/expected-data/walking_morphism.json
@@ -116,6 +116,7 @@
 		"pullbacks",
 		"pushout-stable regular monomorphisms",
 		"pushouts",
+		"quasicotopos",
 		"quasitopos",
 		"quotients of congruences",
 		"reflexive coequalizers",
@@ -172,11 +173,13 @@
 		"disjoint finite coproducts",
 		"disjoint finite products",
 		"disjoint products",
+		"elementary cotopos",
 		"elementary topos",
 		"epi-regular",
 		"essentially discrete",
 		"extensive",
 		"Grothendieck abelian",
+		"Grothendieck cotopos",
 		"Grothendieck topos",
 		"groupoid",
 		"infinitary coextensive",
@@ -186,6 +189,7 @@
 		"normal",
 		"pointed",
 		"preadditive",
+		"precotopos",
 		"pretopos",
 		"quotient object classifier",
 		"quotient-trivial",

diff --git a/shared/history.json b/shared/history.json
@@ -1985,6 +1985,22 @@
 		{
 			"type": "category",
 			"id": "locally ℵ₁-copresentable"
+		},
+		{
+			"type": "category",
+			"id": "elementary cotopos"
+		},
+		{
+			"type": "category",
+			"id": "Grothendieck cotopos"
+		},
+		{
+			"type": "category",
+			"id": "precotopos"
+		},
+		{
+			"type": "category",
+			"id": "quasicotopos"
 		}
 	]
 }