From ae2d93d4053c97aa18df2c8ad0bf0cd6499360d5 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 27 Oct 2026 16:38:27 +0100 Subject: [PATCH 1/5] add elementary cotoposes --- .cspell.json | 7 ++++++- .../category-properties/elementary cotopos.yaml | 14 ++++++++++++++ .../data/category-properties/elementary topos.yaml | 2 +- .../quotient object classifier.yaml | 2 +- database/scripts/expected-data/Ab.json | 1 + database/scripts/expected-data/FinSet.json | 1 + database/scripts/expected-data/N.json | 1 + database/scripts/expected-data/Set.json | 1 + database/scripts/expected-data/Top.json | 1 + .../scripts/expected-data/walking_morphism.json | 1 + shared/history.json | 4 ++++ 11 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 database/data/category-properties/elementary cotopos.yaml diff --git a/.cspell.json b/.cspell.json index 887f72204..b3c6be824 100644 --- a/.cspell.json +++ b/.cspell.json @@ -165,6 +165,7 @@ "cospans", "cosymmetric", "cosymmetry", + "cotopos", "cototal", "cotransitive", "cotransitivity", @@ -453,5 +454,9 @@ "todo.txt", "*.svg" ], - "ignoreRegExpList": ["\\$[^$]*\\$", "\\$\\$[^$]*\\$\\$", "Wahrscheinlichkeitstheorie"] + "ignoreRegExpList": [ + "\\$[^$]*\\$", + "\\$\\$[^$]*\\$\\$", + "Wahrscheinlichkeitstheorie" + ] } diff --git a/database/data/category-properties/elementary cotopos.yaml b/database/data/category-properties/elementary cotopos.yaml new file mode 100644 index 000000000..5f84b3cdb --- /dev/null +++ b/database/data/category-properties/elementary cotopos.yaml @@ -0,0 +1,14 @@ +id: elementary cotopos +relation: is an +description: An elementary cotopos 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 + +tags: + - topos theory diff --git a/database/data/category-properties/elementary topos.yaml b/database/data/category-properties/elementary topos.yaml index f471a7049..8226cbccc 100644 --- a/database/data/category-properties/elementary topos.yaml +++ b/database/data/category-properties/elementary topos.yaml @@ -2,7 +2,7 @@ id: elementary topos relation: is an description: An elementary topos 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: diff --git a/database/data/category-properties/quotient object classifier.yaml b/database/data/category-properties/quotient object classifier.yaml index 600542fac..e55ae8142 100644 --- a/database/data/category-properties/quotient object classifier.yaml +++ b/database/data/category-properties/quotient object classifier.yaml @@ -5,7 +5,7 @@ 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 diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 2c597c82d..2710d538c 100644 --- 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", diff --git a/database/scripts/expected-data/FinSet.json b/database/scripts/expected-data/FinSet.json index dec65c542..b323495aa 100644 --- 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", diff --git a/database/scripts/expected-data/N.json b/database/scripts/expected-data/N.json index 927137cc5..2bb6827c5 100644 --- 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", diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index 181deb0be..da3c1f839 100644 --- 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", diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index a04ba72d0..d42cc68e1 100644 --- 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", diff --git a/database/scripts/expected-data/walking_morphism.json b/database/scripts/expected-data/walking_morphism.json index 3ffd66140..e2b6ae79b 100644 --- a/database/scripts/expected-data/walking_morphism.json +++ b/database/scripts/expected-data/walking_morphism.json @@ -172,6 +172,7 @@ "disjoint finite coproducts", "disjoint finite products", "disjoint products", + "elementary cotopos", "elementary topos", "epi-regular", "essentially discrete", diff --git a/shared/history.json b/shared/history.json index 140b172ab..2b2309d55 100644 --- a/shared/history.json +++ b/shared/history.json @@ -1985,6 +1985,10 @@ { "type": "category", "id": "locally ℵ₁-copresentable" + }, + { + "type": "category", + "id": "elementary cotopos" } ] } From e4bbdf62dfced6f690dff041b7a095cbd2d0bb5d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 27 Oct 2026 16:43:20 +0100 Subject: [PATCH 2/5] add Grothendieck cotoposes --- .../category-properties/Grothendieck cotopos.yaml | 12 ++++++++++++ .../data/category-properties/Grothendieck topos.yaml | 2 +- database/scripts/expected-data/Ab.json | 1 + database/scripts/expected-data/FinSet.json | 1 + database/scripts/expected-data/N.json | 1 + database/scripts/expected-data/Set.json | 1 + database/scripts/expected-data/Top.json | 1 + database/scripts/expected-data/walking_morphism.json | 1 + shared/history.json | 4 ++++ 9 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 database/data/category-properties/Grothendieck cotopos.yaml diff --git a/database/data/category-properties/Grothendieck cotopos.yaml b/database/data/category-properties/Grothendieck cotopos.yaml new file mode 100644 index 000000000..4c9c19714 --- /dev/null +++ b/database/data/category-properties/Grothendieck cotopos.yaml @@ -0,0 +1,12 @@ +id: Grothendieck cotopos +relation: is a +description: A Grothendieck cotopos 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 index 4344078f2..d30869eaf 100644 --- 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 Grothendieck topos 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/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 2710d538c..66ad6d015 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -161,6 +161,7 @@ "finite", "finitely coaccessible", "gaunt", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", diff --git a/database/scripts/expected-data/FinSet.json b/database/scripts/expected-data/FinSet.json index b323495aa..ac67e5940 100644 --- a/database/scripts/expected-data/FinSet.json +++ b/database/scripts/expected-data/FinSet.json @@ -138,6 +138,7 @@ "gaunt", "generalized variety", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", diff --git a/database/scripts/expected-data/N.json b/database/scripts/expected-data/N.json index 2bb6827c5..d12de072c 100644 --- a/database/scripts/expected-data/N.json +++ b/database/scripts/expected-data/N.json @@ -145,6 +145,7 @@ "finitely complete", "generalized variety", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index da3c1f839..4000a572a 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -163,6 +163,7 @@ "finitely coaccessible", "gaunt", "Grothendieck abelian", + "Grothendieck cotopos", "groupoid", "infinitary codistributive", "infinitary coextensive", diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index d42cc68e1..84a7758e0 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -146,6 +146,7 @@ "gaunt", "generalized variety", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", diff --git a/database/scripts/expected-data/walking_morphism.json b/database/scripts/expected-data/walking_morphism.json index e2b6ae79b..4c99b59fc 100644 --- a/database/scripts/expected-data/walking_morphism.json +++ b/database/scripts/expected-data/walking_morphism.json @@ -178,6 +178,7 @@ "essentially discrete", "extensive", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary coextensive", diff --git a/shared/history.json b/shared/history.json index 2b2309d55..fcee56f22 100644 --- a/shared/history.json +++ b/shared/history.json @@ -1989,6 +1989,10 @@ { "type": "category", "id": "elementary cotopos" + }, + { + "type": "category", + "id": "Grothendieck cotopos" } ] } From be6ad898602dd6421592e5a6b4995f9385b9ba5e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 27 Oct 2026 16:52:19 +0100 Subject: [PATCH 3/5] add precotoposes --- .cspell.json | 7 ++----- .../data/category-properties/precotopos.yaml | 16 ++++++++++++++++ database/data/category-properties/pretopos.yaml | 2 +- database/scripts/expected-data/Ab.json | 1 + database/scripts/expected-data/FinSet.json | 1 + database/scripts/expected-data/N.json | 1 + database/scripts/expected-data/Set.json | 1 + database/scripts/expected-data/Top.json | 1 + .../scripts/expected-data/walking_morphism.json | 1 + shared/history.json | 4 ++++ 10 files changed, 29 insertions(+), 6 deletions(-) create mode 100644 database/data/category-properties/precotopos.yaml diff --git a/.cspell.json b/.cspell.json index b3c6be824..d66fda252 100644 --- a/.cspell.json +++ b/.cspell.json @@ -328,6 +328,7 @@ "precomposed", "precomposing", "precomposition", + "precotopos", "preimage", "preimages", "preorder", @@ -454,9 +455,5 @@ "todo.txt", "*.svg" ], - "ignoreRegExpList": [ - "\\$[^$]*\\$", - "\\$\\$[^$]*\\$\\$", - "Wahrscheinlichkeitstheorie" - ] + "ignoreRegExpList": ["\\$[^$]*\\$", "\\$\\$[^$]*\\$\\$", "Wahrscheinlichkeitstheorie"] } diff --git a/database/data/category-properties/precotopos.yaml b/database/data/category-properties/precotopos.yaml new file mode 100644 index 000000000..b1e6321bc --- /dev/null +++ b/database/data/category-properties/precotopos.yaml @@ -0,0 +1,16 @@ +id: precotopos +relation: is a +description: A precotopos 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 index e8820b30f..5a6a0baca 100644 --- 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 pretopos 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/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 66ad6d015..c88083dab 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -178,6 +178,7 @@ "locally ℵ₁-copresentable", "one-way", "parametrized natural numbers object", + "precotopos", "pretopos", "quasitopos", "quotient object classifier", diff --git a/database/scripts/expected-data/FinSet.json b/database/scripts/expected-data/FinSet.json index ac67e5940..b1fd11c7c 100644 --- a/database/scripts/expected-data/FinSet.json +++ b/database/scripts/expected-data/FinSet.json @@ -170,6 +170,7 @@ "pointed", "powers", "preadditive", + "precotopos", "products", "quotient object classifier", "quotient-trivial", diff --git a/database/scripts/expected-data/N.json b/database/scripts/expected-data/N.json index d12de072c..bc9b009b4 100644 --- a/database/scripts/expected-data/N.json +++ b/database/scripts/expected-data/N.json @@ -173,6 +173,7 @@ "pointed", "powers", "preadditive", + "precotopos", "pretopos", "products", "quasitopos", diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index 4000a572a..98a3f0ef3 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -180,6 +180,7 @@ "one-way", "pointed", "preadditive", + "precotopos", "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 index 84a7758e0..ff9493347 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -174,6 +174,7 @@ "one-way", "pointed", "preadditive", + "precotopos", "pretopos", "pullback-stable regular epimorphisms", "quasitopos", diff --git a/database/scripts/expected-data/walking_morphism.json b/database/scripts/expected-data/walking_morphism.json index 4c99b59fc..eed699b56 100644 --- a/database/scripts/expected-data/walking_morphism.json +++ b/database/scripts/expected-data/walking_morphism.json @@ -188,6 +188,7 @@ "normal", "pointed", "preadditive", + "precotopos", "pretopos", "quotient object classifier", "quotient-trivial", diff --git a/shared/history.json b/shared/history.json index fcee56f22..f19a5b1c8 100644 --- a/shared/history.json +++ b/shared/history.json @@ -1993,6 +1993,10 @@ { "type": "category", "id": "Grothendieck cotopos" + }, + { + "type": "category", + "id": "precotopos" } ] } From bcfa782ef9427edcb07c90d94a6d56e72b1c9c17 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 27 Oct 2026 16:56:20 +0100 Subject: [PATCH 4/5] add more property relations --- database/data/category-properties/Barr-coexact.yaml | 1 + database/data/category-properties/coextensive.yaml | 1 + database/data/category-properties/elementary cotopos.yaml | 2 ++ database/data/category-properties/elementary topos.yaml | 4 ++-- .../data/category-properties/quotient object classifier.yaml | 1 + 5 files changed, 7 insertions(+), 2 deletions(-) diff --git a/database/data/category-properties/Barr-coexact.yaml b/database/data/category-properties/Barr-coexact.yaml index 908c04008..5f4a66301 100644 --- 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/coextensive.yaml b/database/data/category-properties/coextensive.yaml index ca5390b71..3be57d838 100644 --- 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 index 5f84b3cdb..4bbe4bafd 100644 --- a/database/data/category-properties/elementary cotopos.yaml +++ b/database/data/category-properties/elementary cotopos.yaml @@ -9,6 +9,8 @@ related: - cocartesian coclosed - finitely cocomplete - quotient object classifier + - Grothendieck cotopos + - precotopos tags: - topos theory diff --git a/database/data/category-properties/elementary topos.yaml b/database/data/category-properties/elementary topos.yaml index 8226cbccc..eb02381cf 100644 --- a/database/data/category-properties/elementary topos.yaml +++ b/database/data/category-properties/elementary topos.yaml @@ -6,13 +6,13 @@ 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/quotient object classifier.yaml b/database/data/category-properties/quotient object classifier.yaml index e55ae8142..265156bf9 100644 --- a/database/data/category-properties/quotient object classifier.yaml +++ b/database/data/category-properties/quotient object classifier.yaml @@ -12,6 +12,7 @@ invariant_under_equivalences: true related: - finitely cocomplete - regular quotient object classifier + - elementary cotopos tags: - topos theory From e15557efaf5b14223ad6dadb95fb93df10ab8986 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 27 Oct 2026 17:07:36 +0100 Subject: [PATCH 5/5] add quasicotoposes --- .cspell.json | 1 + .../elementary cotopos.yaml | 1 + .../category-properties/quasicotopos.yaml | 20 +++++++++++++++++++ .../data/category-properties/quasitopos.yaml | 2 +- .../regular quotient object classifier.yaml | 1 + database/scripts/expected-data/Ab.json | 1 + database/scripts/expected-data/FinSet.json | 1 + database/scripts/expected-data/N.json | 1 + database/scripts/expected-data/Set.json | 1 + database/scripts/expected-data/Top.json | 1 + .../expected-data/walking_morphism.json | 1 + shared/history.json | 4 ++++ 12 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 database/data/category-properties/quasicotopos.yaml diff --git a/.cspell.json b/.cspell.json index d66fda252..56bcf16d4 100644 --- a/.cspell.json +++ b/.cspell.json @@ -350,6 +350,7 @@ "pushforward", "pushout", "pushouts", + "quasicotopos", "quasitopos", "Quillan", "Reggio", diff --git a/database/data/category-properties/elementary cotopos.yaml b/database/data/category-properties/elementary cotopos.yaml index 4bbe4bafd..e0d08d47f 100644 --- a/database/data/category-properties/elementary cotopos.yaml +++ b/database/data/category-properties/elementary cotopos.yaml @@ -11,6 +11,7 @@ related: - quotient object classifier - Grothendieck cotopos - precotopos + - quasitopos tags: - topos theory diff --git a/database/data/category-properties/quasicotopos.yaml b/database/data/category-properties/quasicotopos.yaml new file mode 100644 index 000000000..90ce11ae5 --- /dev/null +++ b/database/data/category-properties/quasicotopos.yaml @@ -0,0 +1,20 @@ +id: quasicotopos +relation: is a +description: >- + A quasicotopos 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 index 82576e47b..3c1130723 100644 --- 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 MSE/4335533. nlab_link: https://ncatlab.org/nlab/show/quasitopos -dual: null +dual: quasicotopos invariant_under_equivalences: true keywords: diff --git a/database/data/category-properties/regular quotient object classifier.yaml b/database/data/category-properties/regular quotient object classifier.yaml index 0d574ab43..ea6f89484 100644 --- 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 index c88083dab..1bf5ffbde 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -180,6 +180,7 @@ "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 index b1fd11c7c..0a10138ec 100644 --- a/database/scripts/expected-data/FinSet.json +++ b/database/scripts/expected-data/FinSet.json @@ -172,6 +172,7 @@ "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 index bc9b009b4..3adbd63da 100644 --- a/database/scripts/expected-data/N.json +++ b/database/scripts/expected-data/N.json @@ -176,6 +176,7 @@ "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 index 98a3f0ef3..e7379ce9e 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -181,6 +181,7 @@ "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 index ff9493347..171186197 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -177,6 +177,7 @@ "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 index eed699b56..241e79180 100644 --- 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", diff --git a/shared/history.json b/shared/history.json index f19a5b1c8..560b3fad0 100644 --- a/shared/history.json +++ b/shared/history.json @@ -1997,6 +1997,10 @@ { "type": "category", "id": "precotopos" + }, + { + "type": "category", + "id": "quasicotopos" } ] }