ScriptRaccoon · ScriptRaccoon · Jul 1, 2026 · Jun 30, 2026 · Jun 30, 2026 · Jul 1, 2026
diff --git a/.cspell.json b/.cspell.json
@@ -26,6 +26,7 @@
 		"abelianize",
 		"Adamek",
 		"adic",
+		"algebraicity",
 		"algébriques",
 		"anneaux",
 		"Artin",
@@ -176,6 +177,7 @@
 		"injections",
 		"injective",
 		"injectivity",
+		"invertibility",
 		"Isbell",
 		"Johnstone",
 		"Jónsson",

diff --git a/DATABASE.md b/DATABASE.md
@@ -108,9 +108,9 @@ to check for redundant assignments of properties to categorical structures.
 
 ## Diagram
 
-This is the database schema as of 17.06.2026; changes may occur.
+This is the database schema as of 01.07.2026; changes may occur.
 
-<img alt="database diagram" src="https://github.com/user-attachments/assets/8625e58a-660b-47f7-8e01-ab74a1286617" />
+<img alt="database diagram" src="https://github.com/user-attachments/assets/cfde0cea-07fa-4538-8ebb-9d97b1c352cc" />
 
 ## Application Database
 

diff --git a/databases/catdat/data/category-properties/Barr-coexact.yaml b/databases/catdat/data/category-properties/Barr-coexact.yaml
@@ -8,3 +8,7 @@ related_properties:
   - coregular
   - effective cocongruences
   - coquotients of cocongruences
+
+tags:
+  - limit–colimit interaction
+  - congruences
diff --git a/databases/catdat/data/category-properties/Barr-exact.yaml b/databases/catdat/data/category-properties/Barr-exact.yaml
@@ -10,3 +10,7 @@ related_properties:
   - effective congruences
   - quotients of congruences
   - pretopos
+
+tags:
+  - limit–colimit interaction
+  - congruences
diff --git a/databases/catdat/data/category-properties/CIP.yaml b/databases/catdat/data/category-properties/CIP.yaml
@@ -14,3 +14,6 @@ related_properties:
   - filtered-colimit-stable monomorphisms
   - products
   - zero morphisms
+
+tags:
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/CSP.yaml b/databases/catdat/data/category-properties/CSP.yaml
@@ -14,3 +14,6 @@ related_properties:
   - products
   - unital
   - zero morphisms
+
+tags:
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/Cauchy complete.yaml b/databases/catdat/data/category-properties/Cauchy complete.yaml
@@ -7,3 +7,8 @@ invariant_under_equivalences: true
 
 related_properties:
   - finitely complete
+
+tags:
+  - limits
+  - colimits
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/Grothendieck abelian.yaml b/databases/catdat/data/category-properties/Grothendieck abelian.yaml
@@ -9,3 +9,6 @@ related_properties:
   - cocomplete
   - exact filtered colimits
   - generator
+
+tags:
+  - abelian
diff --git a/databases/catdat/data/category-properties/Grothendieck topos.yaml b/databases/catdat/data/category-properties/Grothendieck topos.yaml
@@ -6,3 +6,6 @@ invariant_under_equivalences: true
 
 related_properties:
   - elementary topos
+
+tags:
+  - topos theory
diff --git a/databases/catdat/data/category-properties/Malcev.yaml b/databases/catdat/data/category-properties/Malcev.yaml
@@ -7,3 +7,6 @@ invariant_under_equivalences: true
 
 related_properties:
   - finitely complete
+
+tags:
+  - congruences
diff --git a/databases/catdat/data/category-properties/abelian.yaml b/databases/catdat/data/category-properties/abelian.yaml
@@ -11,3 +11,8 @@ related_properties:
   - conormal
   - kernels
   - normal
+  - Grothendieck abelian
+  - split abelian
+
+tags:
+  - abelian
diff --git a/databases/catdat/data/category-properties/accessible.yaml b/databases/catdat/data/category-properties/accessible.yaml
@@ -11,3 +11,6 @@ related_properties:
   - locally poly-presentable
   - locally presentable
   - ℵ₁-accessible
+
+tags:
+  - accessibility
diff --git a/databases/catdat/data/category-properties/additive.yaml b/databases/catdat/data/category-properties/additive.yaml
@@ -10,3 +10,9 @@ related_properties:
   - finite coproducts
   - finite products
   - preadditive
+
+tags:
+  - morphism behavior
+  - limits
+  - colimits
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/aleph1-accessible.yaml b/databases/catdat/data/category-properties/aleph1-accessible.yaml
@@ -9,3 +9,6 @@ related_properties:
   - finitely accessible
   - locally ℵ₁-presentable
   - ℵ₁-filtered colimits
+
+tags:
+  - accessibility
diff --git a/databases/catdat/data/category-properties/aleph1-cofiltered limits.yaml b/databases/catdat/data/category-properties/aleph1-cofiltered limits.yaml
@@ -9,3 +9,6 @@ related_properties:
   - complete
   - cofiltered limits
   - ℵ₁-cofiltered
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/aleph1-cofiltered.yaml b/databases/catdat/data/category-properties/aleph1-cofiltered.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - cofiltered
   - complete
+
+tags:
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml
@@ -10,3 +10,6 @@ related_properties:
   - filtered colimits
   - ℵ₁-accessible
   - ℵ₁-filtered
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/aleph1-filtered.yaml b/databases/catdat/data/category-properties/aleph1-filtered.yaml
@@ -9,3 +9,6 @@ related_properties:
   - filtered
   - ℵ₁-filtered colimits
   - cocomplete
+
+tags:
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/aleph2-small copowers.yaml b/databases/catdat/data/category-properties/aleph2-small copowers.yaml
@@ -12,3 +12,6 @@ related_properties:
   - countable copowers
   - finite copowers
   - ℵ₂-small coproducts
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/aleph2-small coproducts.yaml b/databases/catdat/data/category-properties/aleph2-small coproducts.yaml
@@ -12,3 +12,6 @@ related_properties:
   - countable coproducts
   - finite coproducts
   - ℵ₂-small powers
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/aleph2-small powers.yaml b/databases/catdat/data/category-properties/aleph2-small powers.yaml
@@ -12,3 +12,6 @@ related_properties:
   - countable powers
   - finite powers
   - ℵ₂-small products
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/aleph2-small products.yaml b/databases/catdat/data/category-properties/aleph2-small products.yaml
@@ -12,3 +12,6 @@ related_properties:
   - countable products
   - finite products
   - ℵ₂-small powers
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/balanced.yaml b/databases/catdat/data/category-properties/balanced.yaml
@@ -6,3 +6,6 @@ dual_property: balanced
 invariant_under_equivalences: true
 
 related_properties: []
+
+tags:
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/binary copowers.yaml b/databases/catdat/data/category-properties/binary copowers.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - finite copowers
   - finite coproducts
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/binary coproducts.yaml b/databases/catdat/data/category-properties/binary coproducts.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - binary copowers
   - finite coproducts
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/binary powers.yaml b/databases/catdat/data/category-properties/binary powers.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - finite powers
   - finite products
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/binary products.yaml b/databases/catdat/data/category-properties/binary products.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - binary powers
   - finite products
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/biproducts.yaml b/databases/catdat/data/category-properties/biproducts.yaml
@@ -13,3 +13,8 @@ related_properties:
   - finite coproducts
   - finite products
   - zero morphisms
+
+tags:
+  - limits
+  - colimits
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/cartesian closed.yaml b/databases/catdat/data/category-properties/cartesian closed.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - finite products
   - locally cartesian closed
+
+tags:
+  - topos theory
diff --git a/databases/catdat/data/category-properties/cartesian filtered colimits.yaml b/databases/catdat/data/category-properties/cartesian filtered colimits.yaml
@@ -10,3 +10,6 @@ related_properties:
   - exact filtered colimits
   - filtered colimits
   - finite products
+
+tags:
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/co-Malcev.yaml b/databases/catdat/data/category-properties/co-Malcev.yaml
@@ -9,3 +9,6 @@ invariant_under_equivalences: true
 
 related_properties:
   - finitely cocomplete
+
+tags:
+  - congruences
diff --git a/databases/catdat/data/category-properties/coaccessible.yaml b/databases/catdat/data/category-properties/coaccessible.yaml
@@ -6,3 +6,6 @@ invariant_under_equivalences: true
 
 related_properties:
   - locally copresentable
+
+tags:
+  - accessibility
diff --git a/databases/catdat/data/category-properties/cocartesian coclosed.yaml b/databases/catdat/data/category-properties/cocartesian coclosed.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - finite coproducts
   - locally cocartesian coclosed
+
+tags:
+  - topos theory
diff --git a/databases/catdat/data/category-properties/cocartesian cofiltered limits.yaml b/databases/catdat/data/category-properties/cocartesian cofiltered limits.yaml
@@ -10,3 +10,6 @@ related_properties:
   - cofiltered limits
   - exact cofiltered limits
   - finite coproducts
+
+tags:
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/cocomplete.yaml b/databases/catdat/data/category-properties/cocomplete.yaml
@@ -9,3 +9,6 @@ related_properties:
   - coequalizers
   - coproducts
   - multi-cocomplete
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/codistributive.yaml b/databases/catdat/data/category-properties/codistributive.yaml
@@ -9,3 +9,6 @@ related_properties:
   - finite coproducts
   - finite products
   - infinitary codistributive
+
+tags:
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/coequalizers.yaml b/databases/catdat/data/category-properties/coequalizers.yaml
@@ -10,3 +10,6 @@ related_properties:
   - finitely cocomplete
   - quotients of congruences
   - reflexive coequalizers
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/coextensive.yaml b/databases/catdat/data/category-properties/coextensive.yaml
@@ -8,3 +8,6 @@ related_properties:
   - disjoint finite products
   - finite products
   - infinitary coextensive
+
+tags:
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/cofiltered limits.yaml b/databases/catdat/data/category-properties/cofiltered limits.yaml
@@ -10,3 +10,6 @@ related_properties:
   - complete
   - cosifted limits
   - directed limits
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/cofiltered-limit-stable epimorphisms.yaml b/databases/catdat/data/category-properties/cofiltered-limit-stable epimorphisms.yaml
@@ -7,3 +7,7 @@ invariant_under_equivalences: true
 related_properties:
   - cofiltered limits
   - exact cofiltered limits
+
+tags:
+  - morphism behavior
+  - limit–colimit interaction
diff --git a/databases/catdat/data/category-properties/cofiltered.yaml b/databases/catdat/data/category-properties/cofiltered.yaml
@@ -8,3 +8,6 @@ invariant_under_equivalences: true
 related_properties:
   - cofiltered limits
   - finitely complete
+
+tags:
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/cogenerating set.yaml b/databases/catdat/data/category-properties/cogenerating set.yaml
@@ -7,3 +7,6 @@ invariant_under_equivalences: true
 
 related_properties:
   - cogenerator
+
+tags:
+  - size
diff --git a/databases/catdat/data/category-properties/cogenerator.yaml b/databases/catdat/data/category-properties/cogenerator.yaml
@@ -7,3 +7,7 @@ invariant_under_equivalences: true
 
 related_properties:
   - cogenerating set
+
+tags:
+  - morphism behavior
+  - size
diff --git a/databases/catdat/data/category-properties/cokernels.yaml b/databases/catdat/data/category-properties/cokernels.yaml
@@ -10,3 +10,6 @@ related_properties:
   - conormal
   - quotients of congruences
   - zero morphisms
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/complete.yaml b/databases/catdat/data/category-properties/complete.yaml
@@ -9,3 +9,6 @@ related_properties:
   - equalizers
   - multi-complete
   - products
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/connected colimits.yaml b/databases/catdat/data/category-properties/connected colimits.yaml
@@ -9,3 +9,6 @@ related_properties:
   - cocomplete
   - connected
   - filtered colimits
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/connected limits.yaml b/databases/catdat/data/category-properties/connected limits.yaml
@@ -9,3 +9,6 @@ related_properties:
   - cofiltered limits
   - complete
   - connected
+
+tags:
+  - limits
diff --git a/databases/catdat/data/category-properties/connected.yaml b/databases/catdat/data/category-properties/connected.yaml
@@ -9,3 +9,6 @@ related_properties:
   - inhabited
   - semi-strongly connected
   - strongly connected
+
+tags:
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/conormal.yaml b/databases/catdat/data/category-properties/conormal.yaml
@@ -10,3 +10,6 @@ related_properties:
   - effective cocongruences
   - epi-regular
   - zero morphisms
+
+tags:
+  - morphism behavior
diff --git a/databases/catdat/data/category-properties/copowers.yaml b/databases/catdat/data/category-properties/copowers.yaml
@@ -9,3 +9,6 @@ related_properties:
   - coproducts
   - countable copowers
   - finite copowers
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/coproducts.yaml b/databases/catdat/data/category-properties/coproducts.yaml
@@ -9,3 +9,6 @@ related_properties:
   - cocomplete
   - copowers
   - finite coproducts
+
+tags:
+  - colimits
diff --git a/databases/catdat/data/category-properties/coquotients of cocongruences.yaml b/databases/catdat/data/category-properties/coquotients of cocongruences.yaml
@@ -10,3 +10,7 @@ related_properties:
   - equalizers
   - kernels
   - Barr-coexact
+
+tags:
+  - limits
+  - congruences
diff --git a/databases/catdat/data/category-properties/core-thin.yaml b/databases/catdat/data/category-properties/core-thin.yaml
@@ -15,3 +15,6 @@ related_properties:
   - gaunt
   - one-way
   - thin
+
+tags:
+  - morphism behavior
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,3 +7,6 @@ invariant_under_equivalences: true @@
     related_properties:
       - cogenerator
+    tags:
+      - size