diff --git a/databases/catdat/data/categories/0.yaml b/databases/catdat/data/categories/0.yaml index 771cbe18..9357778d 100644 --- a/databases/catdat/data/categories/0.yaml +++ b/databases/catdat/data/categories/0.yaml @@ -10,7 +10,7 @@ tags: - finite - thin -related_categories: +related: - '1' satisfied_properties: diff --git a/databases/catdat/data/categories/1.yaml b/databases/catdat/data/categories/1.yaml index 24234f5c..80fd1c24 100644 --- a/databases/catdat/data/categories/1.yaml +++ b/databases/catdat/data/categories/1.yaml @@ -11,7 +11,7 @@ tags: - single object - thin -related_categories: +related: - '0' - '2' diff --git a/databases/catdat/data/categories/2.yaml b/databases/catdat/data/categories/2.yaml index 07a72f4b..5f87cd54 100644 --- a/databases/catdat/data/categories/2.yaml +++ b/databases/catdat/data/categories/2.yaml @@ -10,7 +10,7 @@ tags: - finite - thin -related_categories: +related: - '1' satisfied_properties: diff --git a/databases/catdat/data/categories/Ab.yaml b/databases/catdat/data/categories/Ab.yaml index 524b5f2b..15239fb9 100644 --- a/databases/catdat/data/categories/Ab.yaml +++ b/databases/catdat/data/categories/Ab.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Ab tags: - algebra -related_categories: +related: - Ab_fg - CMon - FinAb diff --git a/databases/catdat/data/categories/Ab_fg.yaml b/databases/catdat/data/categories/Ab_fg.yaml index d9f65472..a60adbaf 100644 --- a/databases/catdat/data/categories/Ab_fg.yaml +++ b/databases/catdat/data/categories/Ab_fg.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/finitely+generated+module tags: - algebra -related_categories: +related: - Ab - FinAb diff --git a/databases/catdat/data/categories/Alg(R).yaml b/databases/catdat/data/categories/Alg(R).yaml index d6632b4e..49553a10 100644 --- a/databases/catdat/data/categories/Alg(R).yaml +++ b/databases/catdat/data/categories/Alg(R).yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Alg tags: - algebra -related_categories: +related: - CAlg(R) - R-Mod - Ring diff --git a/databases/catdat/data/categories/B.yaml b/databases/catdat/data/categories/B.yaml index 66ef6c3f..ede73eb1 100644 --- a/databases/catdat/data/categories/B.yaml +++ b/databases/catdat/data/categories/B.yaml @@ -10,7 +10,7 @@ tags: - combinatorics - set theory -related_categories: +related: - FI - FS diff --git a/databases/catdat/data/categories/BG_c.yaml b/databases/catdat/data/categories/BG_c.yaml index 09cf7148..356c3394 100644 --- a/databases/catdat/data/categories/BG_c.yaml +++ b/databases/catdat/data/categories/BG_c.yaml @@ -11,7 +11,7 @@ tags: - category theory - single object -related_categories: +related: - BG_f - BN diff --git a/databases/catdat/data/categories/BG_f.yaml b/databases/catdat/data/categories/BG_f.yaml index d1bcf885..e3db568d 100644 --- a/databases/catdat/data/categories/BG_f.yaml +++ b/databases/catdat/data/categories/BG_f.yaml @@ -12,7 +12,7 @@ tags: - finite - single object -related_categories: +related: - BG_c - BN diff --git a/databases/catdat/data/categories/BN.yaml b/databases/catdat/data/categories/BN.yaml index 44a1b7c1..1ce7785d 100644 --- a/databases/catdat/data/categories/BN.yaml +++ b/databases/catdat/data/categories/BN.yaml @@ -11,7 +11,7 @@ tags: - number theory - single object -related_categories: +related: - BG_c - BOn diff --git a/databases/catdat/data/categories/BOn.yaml b/databases/catdat/data/categories/BOn.yaml index 04ee602d..4eb49d20 100644 --- a/databases/catdat/data/categories/BOn.yaml +++ b/databases/catdat/data/categories/BOn.yaml @@ -10,7 +10,7 @@ tags: - set theory - single object -related_categories: +related: - BN satisfied_properties: diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index 92fef27f..e77d7aab 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Banach+space tags: - analysis -related_categories: +related: - Met satisfied_properties: diff --git a/databases/catdat/data/categories/CAlg(R).yaml b/databases/catdat/data/categories/CAlg(R).yaml index 0244eb45..e375c4a0 100644 --- a/databases/catdat/data/categories/CAlg(R).yaml +++ b/databases/catdat/data/categories/CAlg(R).yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/CommAlg tags: - algebra -related_categories: +related: - Alg(R) - CRing - R-Mod diff --git a/databases/catdat/data/categories/CMon.yaml b/databases/catdat/data/categories/CMon.yaml index 28f5eb2b..d8f955ba 100644 --- a/databases/catdat/data/categories/CMon.yaml +++ b/databases/catdat/data/categories/CMon.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/category+of+monoids tags: - algebra -related_categories: +related: - Ab - CRing - Mon diff --git a/databases/catdat/data/categories/CRing.yaml b/databases/catdat/data/categories/CRing.yaml index d95061e9..63995170 100644 --- a/databases/catdat/data/categories/CRing.yaml +++ b/databases/catdat/data/categories/CRing.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/CRing tags: - algebra -related_categories: +related: - CAlg(R) - Ring - Rng diff --git a/databases/catdat/data/categories/Cat.yaml b/databases/catdat/data/categories/Cat.yaml index 3d1f40ef..c1ca185a 100644 --- a/databases/catdat/data/categories/Cat.yaml +++ b/databases/catdat/data/categories/Cat.yaml @@ -10,7 +10,7 @@ tags: - algebra - category theory -related_categories: +related: - Mon - Set diff --git a/databases/catdat/data/categories/CompHaus.yaml b/databases/catdat/data/categories/CompHaus.yaml index 4e3e5bde..fe8d5019 100644 --- a/databases/catdat/data/categories/CompHaus.yaml +++ b/databases/catdat/data/categories/CompHaus.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/compact+Hausdorff+space tags: - topology -related_categories: +related: - Haus - Top diff --git a/databases/catdat/data/categories/Delta.yaml b/databases/catdat/data/categories/Delta.yaml index 48958ccf..3a2f1f47 100644 --- a/databases/catdat/data/categories/Delta.yaml +++ b/databases/catdat/data/categories/Delta.yaml @@ -11,7 +11,7 @@ tags: - order theory - topology -related_categories: +related: - FinOrd - Setne - sSet diff --git a/databases/catdat/data/categories/FI.yaml b/databases/catdat/data/categories/FI.yaml index e8f3eb6a..2cafd3fe 100644 --- a/databases/catdat/data/categories/FI.yaml +++ b/databases/catdat/data/categories/FI.yaml @@ -10,7 +10,7 @@ tags: - combinatorics - set theory -related_categories: +related: - B - FS - FinSet diff --git a/databases/catdat/data/categories/FS.yaml b/databases/catdat/data/categories/FS.yaml index d71480e6..dbabae12 100644 --- a/databases/catdat/data/categories/FS.yaml +++ b/databases/catdat/data/categories/FS.yaml @@ -10,7 +10,7 @@ tags: - combinatorics - set theory -related_categories: +related: - B - FI - FinSet diff --git a/databases/catdat/data/categories/FinAb.yaml b/databases/catdat/data/categories/FinAb.yaml index 0b70e319..f6545809 100644 --- a/databases/catdat/data/categories/FinAb.yaml +++ b/databases/catdat/data/categories/FinAb.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/finite+abelian+group tags: - algebra -related_categories: +related: - Ab - Ab_fg - FinGrp diff --git a/databases/catdat/data/categories/FinGrp.yaml b/databases/catdat/data/categories/FinGrp.yaml index 5ce549b5..b93c29bd 100644 --- a/databases/catdat/data/categories/FinGrp.yaml +++ b/databases/catdat/data/categories/FinGrp.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/finite+group tags: - algebra -related_categories: +related: - FinAb - Grp - Grp_c diff --git a/databases/catdat/data/categories/FinOrd.yaml b/databases/catdat/data/categories/FinOrd.yaml index 7843a18b..bb51992f 100644 --- a/databases/catdat/data/categories/FinOrd.yaml +++ b/databases/catdat/data/categories/FinOrd.yaml @@ -10,7 +10,7 @@ tags: - order theory - topology -related_categories: +related: - Delta - FinSet - Pos diff --git a/databases/catdat/data/categories/FinSet.yaml b/databases/catdat/data/categories/FinSet.yaml index b426beb0..354c6ff6 100644 --- a/databases/catdat/data/categories/FinSet.yaml +++ b/databases/catdat/data/categories/FinSet.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/FinSet tags: - set theory -related_categories: +related: - FI - FS - Set diff --git a/databases/catdat/data/categories/Fld.yaml b/databases/catdat/data/categories/Fld.yaml index 950524c1..561632a8 100644 --- a/databases/catdat/data/categories/Fld.yaml +++ b/databases/catdat/data/categories/Fld.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Field tags: - algebra -related_categories: +related: - CRing comments: diff --git a/databases/catdat/data/categories/FreeAb.yaml b/databases/catdat/data/categories/FreeAb.yaml index 5bb22019..30c80eff 100644 --- a/databases/catdat/data/categories/FreeAb.yaml +++ b/databases/catdat/data/categories/FreeAb.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - algebra -related_categories: +related: - Ab - TorsFreeAb diff --git a/databases/catdat/data/categories/Grp.yaml b/databases/catdat/data/categories/Grp.yaml index 453dacf8..aefbbed4 100644 --- a/databases/catdat/data/categories/Grp.yaml +++ b/databases/catdat/data/categories/Grp.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Grp tags: - algebra -related_categories: +related: - FinGrp - Grp_c - Ab diff --git a/databases/catdat/data/categories/Grp_c.yaml b/databases/catdat/data/categories/Grp_c.yaml index ca1b1eeb..5143ab25 100644 --- a/databases/catdat/data/categories/Grp_c.yaml +++ b/databases/catdat/data/categories/Grp_c.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - algebra -related_categories: +related: - Grp - FinGrp - Set_c diff --git a/databases/catdat/data/categories/Haus.yaml b/databases/catdat/data/categories/Haus.yaml index c71cfcda..3035c504 100644 --- a/databases/catdat/data/categories/Haus.yaml +++ b/databases/catdat/data/categories/Haus.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Hausdorff+space tags: - topology -related_categories: +related: - Met_c - Top - CompHaus diff --git a/databases/catdat/data/categories/J2.yaml b/databases/catdat/data/categories/J2.yaml index 9a58794b..2acf5412 100644 --- a/databases/catdat/data/categories/J2.yaml +++ b/databases/catdat/data/categories/J2.yaml @@ -12,7 +12,7 @@ tags: - algebra - set theory -related_categories: +related: - M-Set satisfied_properties: diff --git a/databases/catdat/data/categories/LRS_R.yaml b/databases/catdat/data/categories/LRS_R.yaml index 112b01fe..2aa238a4 100644 --- a/databases/catdat/data/categories/LRS_R.yaml +++ b/databases/catdat/data/categories/LRS_R.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/locally+ringed+topological+space tags: - algebraic geometry -related_categories: +related: - Sch_R satisfied_properties: diff --git a/databases/catdat/data/categories/M-Set.yaml b/databases/catdat/data/categories/M-Set.yaml index aba43771..0ae463c4 100644 --- a/databases/catdat/data/categories/M-Set.yaml +++ b/databases/catdat/data/categories/M-Set.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/MSet tags: - algebra -related_categories: +related: - J2 - R-Mod - Set diff --git a/databases/catdat/data/categories/Man.yaml b/databases/catdat/data/categories/Man.yaml index 5583ac3d..e3e6a664 100644 --- a/databases/catdat/data/categories/Man.yaml +++ b/databases/catdat/data/categories/Man.yaml @@ -10,7 +10,7 @@ tags: - analysis - topology -related_categories: +related: - Haus - Top diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index c9710ff5..d8e9e124 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Meas tags: - analysis -related_categories: +related: - Top comments: diff --git a/databases/catdat/data/categories/Met.yaml b/databases/catdat/data/categories/Met.yaml index 79c431f9..942abdf7 100644 --- a/databases/catdat/data/categories/Met.yaml +++ b/databases/catdat/data/categories/Met.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Met tags: - analysis -related_categories: +related: - Ban - Met_c - Met_oo diff --git a/databases/catdat/data/categories/Met_c.yaml b/databases/catdat/data/categories/Met_c.yaml index e49fe64f..74e9dd02 100644 --- a/databases/catdat/data/categories/Met_c.yaml +++ b/databases/catdat/data/categories/Met_c.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/metrisable+topological+space tags: - analysis -related_categories: +related: - Haus - Met - Met_oo diff --git a/databases/catdat/data/categories/Met_oo.yaml b/databases/catdat/data/categories/Met_oo.yaml index 74fa5c9b..5b5f350b 100644 --- a/databases/catdat/data/categories/Met_oo.yaml +++ b/databases/catdat/data/categories/Met_oo.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Met tags: - analysis -related_categories: +related: - Met - Met_c diff --git a/databases/catdat/data/categories/Mon.yaml b/databases/catdat/data/categories/Mon.yaml index 4647b42c..6644c410 100644 --- a/databases/catdat/data/categories/Mon.yaml +++ b/databases/catdat/data/categories/Mon.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/category+of+monoids tags: - algebra -related_categories: +related: - CMon - Cat - Grp diff --git a/databases/catdat/data/categories/N.yaml b/databases/catdat/data/categories/N.yaml index 9666758e..d9aaeea0 100644 --- a/databases/catdat/data/categories/N.yaml +++ b/databases/catdat/data/categories/N.yaml @@ -10,7 +10,7 @@ tags: - number theory - thin -related_categories: +related: - N_oo - On - Z_div diff --git a/databases/catdat/data/categories/N_oo.yaml b/databases/catdat/data/categories/N_oo.yaml index e995d53e..d7bb6e07 100644 --- a/databases/catdat/data/categories/N_oo.yaml +++ b/databases/catdat/data/categories/N_oo.yaml @@ -10,7 +10,7 @@ tags: - number theory - thin -related_categories: +related: - N - On diff --git a/databases/catdat/data/categories/On.yaml b/databases/catdat/data/categories/On.yaml index 5f67174e..5da769af 100644 --- a/databases/catdat/data/categories/On.yaml +++ b/databases/catdat/data/categories/On.yaml @@ -10,7 +10,7 @@ tags: - set theory - thin -related_categories: +related: - N satisfied_properties: diff --git a/databases/catdat/data/categories/PMet.yaml b/databases/catdat/data/categories/PMet.yaml index 2811b73a..9ceac19e 100644 --- a/databases/catdat/data/categories/PMet.yaml +++ b/databases/catdat/data/categories/PMet.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - analysis -related_categories: +related: - Met satisfied_properties: diff --git a/databases/catdat/data/categories/Pos.yaml b/databases/catdat/data/categories/Pos.yaml index 5e46bcea..ba9f7f06 100644 --- a/databases/catdat/data/categories/Pos.yaml +++ b/databases/catdat/data/categories/Pos.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Pos tags: - order theory -related_categories: +related: - FinOrd - Prost diff --git a/databases/catdat/data/categories/Prost.yaml b/databases/catdat/data/categories/Prost.yaml index 5db0c545..e54a3c41 100644 --- a/databases/catdat/data/categories/Prost.yaml +++ b/databases/catdat/data/categories/Prost.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Prost tags: - order theory -related_categories: +related: - Pos satisfied_properties: diff --git a/databases/catdat/data/categories/R-Mod.yaml b/databases/catdat/data/categories/R-Mod.yaml index 4db5172e..be24498c 100644 --- a/databases/catdat/data/categories/R-Mod.yaml +++ b/databases/catdat/data/categories/R-Mod.yaml @@ -10,7 +10,7 @@ nlab_link: https://ncatlab.org/nlab/show/module tags: - algebra -related_categories: +related: - Ab - M-Set - R-Mod_div diff --git a/databases/catdat/data/categories/R-Mod_div.yaml b/databases/catdat/data/categories/R-Mod_div.yaml index 2ded4fc7..f03b2056 100644 --- a/databases/catdat/data/categories/R-Mod_div.yaml +++ b/databases/catdat/data/categories/R-Mod_div.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/module tags: - algebra -related_categories: +related: - R-Mod - Vect diff --git a/databases/catdat/data/categories/Rel.yaml b/databases/catdat/data/categories/Rel.yaml index 4cc39835..e01269cb 100644 --- a/databases/catdat/data/categories/Rel.yaml +++ b/databases/catdat/data/categories/Rel.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Rel tags: - set theory -related_categories: +related: - Set satisfied_properties: diff --git a/databases/catdat/data/categories/Ring.yaml b/databases/catdat/data/categories/Ring.yaml index 2798a58b..841abb1b 100644 --- a/databases/catdat/data/categories/Ring.yaml +++ b/databases/catdat/data/categories/Ring.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Ring tags: - algebra -related_categories: +related: - Alg(R) - CRing - Rng diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index b1ad2b70..09941ed5 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Rng tags: - algebra -related_categories: +related: - CRing - Ring diff --git a/databases/catdat/data/categories/Sch_R.yaml b/databases/catdat/data/categories/Sch_R.yaml index 29dc8756..7269a7dd 100644 --- a/databases/catdat/data/categories/Sch_R.yaml +++ b/databases/catdat/data/categories/Sch_R.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/scheme tags: - algebraic geometry -related_categories: +related: - LRS_R - Z diff --git a/databases/catdat/data/categories/SemiGrp.yaml b/databases/catdat/data/categories/SemiGrp.yaml index 1f699617..d1649c9b 100644 --- a/databases/catdat/data/categories/SemiGrp.yaml +++ b/databases/catdat/data/categories/SemiGrp.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/semigroup tags: - algebra -related_categories: +related: - Grp - Mon diff --git a/databases/catdat/data/categories/Set.yaml b/databases/catdat/data/categories/Set.yaml index 8008f4f3..65324d93 100644 --- a/databases/catdat/data/categories/Set.yaml +++ b/databases/catdat/data/categories/Set.yaml @@ -10,7 +10,7 @@ dual_category: Set_op tags: - set theory -related_categories: +related: - FinSet - Set* - Set_c diff --git a/databases/catdat/data/categories/Set_c.yaml b/databases/catdat/data/categories/Set_c.yaml index 52c7186e..b75f74e0 100644 --- a/databases/catdat/data/categories/Set_c.yaml +++ b/databases/catdat/data/categories/Set_c.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - set theory -related_categories: +related: - FinSet - Set - Grp_c diff --git a/databases/catdat/data/categories/Set_f.yaml b/databases/catdat/data/categories/Set_f.yaml index 7b70263f..3401abf6 100644 --- a/databases/catdat/data/categories/Set_f.yaml +++ b/databases/catdat/data/categories/Set_f.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - set theory -related_categories: +related: - FinSet - Set diff --git a/databases/catdat/data/categories/Set_op.yaml b/databases/catdat/data/categories/Set_op.yaml index c6980355..c003d0c1 100644 --- a/databases/catdat/data/categories/Set_op.yaml +++ b/databases/catdat/data/categories/Set_op.yaml @@ -10,7 +10,7 @@ dual_category: Set tags: - set theory -related_categories: [] +related: [] satisfied_properties: [] diff --git a/databases/catdat/data/categories/Set_pointed.yaml b/databases/catdat/data/categories/Set_pointed.yaml index 23a04e53..792de6da 100644 --- a/databases/catdat/data/categories/Set_pointed.yaml +++ b/databases/catdat/data/categories/Set_pointed.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/pointed+set tags: - set theory -related_categories: +related: - Set - Top* diff --git a/databases/catdat/data/categories/Setne.yaml b/databases/catdat/data/categories/Setne.yaml index 373584a0..e456e519 100644 --- a/databases/catdat/data/categories/Setne.yaml +++ b/databases/catdat/data/categories/Setne.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/inhabited+set tags: - set theory -related_categories: +related: - Set satisfied_properties: diff --git a/databases/catdat/data/categories/SetxSet.yaml b/databases/catdat/data/categories/SetxSet.yaml index e16932f7..422d1e03 100644 --- a/databases/catdat/data/categories/SetxSet.yaml +++ b/databases/catdat/data/categories/SetxSet.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - set theory -related_categories: +related: - Set - Sh(X) diff --git a/databases/catdat/data/categories/Sh(X).yaml b/databases/catdat/data/categories/Sh(X).yaml index 507d4795..135caf7b 100644 --- a/databases/catdat/data/categories/Sh(X).yaml +++ b/databases/catdat/data/categories/Sh(X).yaml @@ -10,7 +10,7 @@ tags: - algebraic geometry - topology -related_categories: +related: - Set - SetxSet - Sh(X,Ab) diff --git a/databases/catdat/data/categories/Sh(X,Ab).yaml b/databases/catdat/data/categories/Sh(X,Ab).yaml index 5f76b7b2..7a7c6804 100644 --- a/databases/catdat/data/categories/Sh(X,Ab).yaml +++ b/databases/catdat/data/categories/Sh(X,Ab).yaml @@ -10,7 +10,7 @@ tags: - algebraic geometry - topology -related_categories: +related: - Ab - Sh(X) diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 8e20741e..755bec44 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/databases/catdat/data/categories/Sp.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/species tags: - combinatorics -related_categories: +related: - B - FinSet diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index 56f8cd0f..1fc954a8 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -10,7 +10,7 @@ dual_category: Top_op tags: - topology -related_categories: +related: - Haus - Met_c - Top* diff --git a/databases/catdat/data/categories/Top_op.yaml b/databases/catdat/data/categories/Top_op.yaml index 07c3d4cc..834159f0 100644 --- a/databases/catdat/data/categories/Top_op.yaml +++ b/databases/catdat/data/categories/Top_op.yaml @@ -10,7 +10,7 @@ dual_category: Top tags: - topology -related_categories: [] +related: [] satisfied_properties: [] diff --git a/databases/catdat/data/categories/Top_pointed.yaml b/databases/catdat/data/categories/Top_pointed.yaml index 966e2ed7..e7aecd39 100644 --- a/databases/catdat/data/categories/Top_pointed.yaml +++ b/databases/catdat/data/categories/Top_pointed.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/pointed+topological+space tags: - topology -related_categories: +related: - Set* - Top diff --git a/databases/catdat/data/categories/TorsAb.yaml b/databases/catdat/data/categories/TorsAb.yaml index 89951137..ed433f2d 100644 --- a/databases/catdat/data/categories/TorsAb.yaml +++ b/databases/catdat/data/categories/TorsAb.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/torsion+subgroup tags: - algebra -related_categories: +related: - Ab - FinAb - TorsFreeAb diff --git a/databases/catdat/data/categories/TorsFreeAb.yaml b/databases/catdat/data/categories/TorsFreeAb.yaml index ad3d87e4..9a677c92 100644 --- a/databases/catdat/data/categories/TorsFreeAb.yaml +++ b/databases/catdat/data/categories/TorsFreeAb.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/torsion-free+module tags: - algebra -related_categories: +related: - Ab - FreeAb - TorsAb diff --git a/databases/catdat/data/categories/Vect.yaml b/databases/catdat/data/categories/Vect.yaml index 68e5fc6b..12194aaf 100644 --- a/databases/catdat/data/categories/Vect.yaml +++ b/databases/catdat/data/categories/Vect.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/Vect tags: - algebra -related_categories: +related: - R-Mod - R-Mod_div diff --git a/databases/catdat/data/categories/Z.yaml b/databases/catdat/data/categories/Z.yaml index 1be7b099..0c44fd25 100644 --- a/databases/catdat/data/categories/Z.yaml +++ b/databases/catdat/data/categories/Z.yaml @@ -10,7 +10,7 @@ tags: - algebraic geometry - category theory -related_categories: +related: - Sch_R - Set diff --git a/databases/catdat/data/categories/Z_div.yaml b/databases/catdat/data/categories/Z_div.yaml index 1e1fdf41..9b759dc4 100644 --- a/databases/catdat/data/categories/Z_div.yaml +++ b/databases/catdat/data/categories/Z_div.yaml @@ -10,7 +10,7 @@ tags: - number theory - thin -related_categories: +related: - N satisfied_properties: diff --git a/databases/catdat/data/categories/real_interval.yaml b/databases/catdat/data/categories/real_interval.yaml index b4efb800..fd16c8e0 100644 --- a/databases/catdat/data/categories/real_interval.yaml +++ b/databases/catdat/data/categories/real_interval.yaml @@ -10,7 +10,7 @@ tags: - analysis - thin -related_categories: +related: - N_oo satisfied_properties: diff --git a/databases/catdat/data/categories/sSet.yaml b/databases/catdat/data/categories/sSet.yaml index 55bffc15..5fe32a96 100644 --- a/databases/catdat/data/categories/sSet.yaml +++ b/databases/catdat/data/categories/sSet.yaml @@ -10,7 +10,7 @@ tags: - category theory - topology -related_categories: +related: - Delta - Top diff --git a/databases/catdat/data/categories/walking_commutative_square.yaml b/databases/catdat/data/categories/walking_commutative_square.yaml index 7b6eab27..cf42eb6c 100644 --- a/databases/catdat/data/categories/walking_commutative_square.yaml +++ b/databases/catdat/data/categories/walking_commutative_square.yaml @@ -13,7 +13,7 @@ tags: - finite - thin -related_categories: +related: - walking_fork - walking_morphism diff --git a/databases/catdat/data/categories/walking_composable_pair.yaml b/databases/catdat/data/categories/walking_composable_pair.yaml index 928c5005..63451877 100644 --- a/databases/catdat/data/categories/walking_composable_pair.yaml +++ b/databases/catdat/data/categories/walking_composable_pair.yaml @@ -13,7 +13,7 @@ tags: - finite - thin -related_categories: +related: - walking_fork - walking_morphism diff --git a/databases/catdat/data/categories/walking_coreflexive_pair.yaml b/databases/catdat/data/categories/walking_coreflexive_pair.yaml index f8973452..75077af7 100644 --- a/databases/catdat/data/categories/walking_coreflexive_pair.yaml +++ b/databases/catdat/data/categories/walking_coreflexive_pair.yaml @@ -12,7 +12,7 @@ tags: - category theory - finite -related_categories: +related: - Delta - walking_pair - walking_splitting diff --git a/databases/catdat/data/categories/walking_fork.yaml b/databases/catdat/data/categories/walking_fork.yaml index 85ba7edf..a0d294e3 100644 --- a/databases/catdat/data/categories/walking_fork.yaml +++ b/databases/catdat/data/categories/walking_fork.yaml @@ -12,7 +12,7 @@ tags: - category theory - finite -related_categories: +related: - walking_commutative_square - walking_composable_pair - walking_pair diff --git a/databases/catdat/data/categories/walking_idempotent.yaml b/databases/catdat/data/categories/walking_idempotent.yaml index 41e1cefc..83ecf00a 100644 --- a/databases/catdat/data/categories/walking_idempotent.yaml +++ b/databases/catdat/data/categories/walking_idempotent.yaml @@ -11,7 +11,7 @@ tags: - finite - single object -related_categories: +related: - BG_f - walking_isomorphism - walking_morphism diff --git a/databases/catdat/data/categories/walking_isomorphism.yaml b/databases/catdat/data/categories/walking_isomorphism.yaml index b2e58e6e..1fc047b0 100644 --- a/databases/catdat/data/categories/walking_isomorphism.yaml +++ b/databases/catdat/data/categories/walking_isomorphism.yaml @@ -13,7 +13,7 @@ tags: - finite - thin -related_categories: +related: - '1' - walking_idempotent - walking_morphism diff --git a/databases/catdat/data/categories/walking_morphism.yaml b/databases/catdat/data/categories/walking_morphism.yaml index f03f6e87..30e652a4 100644 --- a/databases/catdat/data/categories/walking_morphism.yaml +++ b/databases/catdat/data/categories/walking_morphism.yaml @@ -13,7 +13,7 @@ tags: - finite - thin -related_categories: +related: - walking_commutative_square - walking_composable_pair - walking_idempotent diff --git a/databases/catdat/data/categories/walking_pair.yaml b/databases/catdat/data/categories/walking_pair.yaml index 86e2b597..50565627 100644 --- a/databases/catdat/data/categories/walking_pair.yaml +++ b/databases/catdat/data/categories/walking_pair.yaml @@ -12,7 +12,7 @@ tags: - category theory - finite -related_categories: +related: - walking_coreflexive_pair - walking_fork - walking_morphism diff --git a/databases/catdat/data/categories/walking_span.yaml b/databases/catdat/data/categories/walking_span.yaml index a6a74142..9bbaf4b2 100644 --- a/databases/catdat/data/categories/walking_span.yaml +++ b/databases/catdat/data/categories/walking_span.yaml @@ -13,7 +13,7 @@ tags: - finite - thin -related_categories: +related: - walking_morphism - walking_pair diff --git a/databases/catdat/data/categories/walking_splitting.yaml b/databases/catdat/data/categories/walking_splitting.yaml index 2f1ef17b..403c6c6d 100644 --- a/databases/catdat/data/categories/walking_splitting.yaml +++ b/databases/catdat/data/categories/walking_splitting.yaml @@ -11,7 +11,7 @@ tags: - category theory - finite -related_categories: +related: - walking_coreflexive_pair - walking_idempotent - walking_isomorphism diff --git a/databases/catdat/data/functor-implications/adjoints.yaml b/databases/catdat/data/functor-implications/adjoints.yaml index d1b8ebbb..abd14f5b 100644 --- a/databases/catdat/data/functor-implications/adjoints.yaml +++ b/databases/catdat/data/functor-implications/adjoints.yaml @@ -1,8 +1,6 @@ - id: right_adjoint_consequences assumptions: - right adjoint - source_assumptions: [] - target_assumptions: [] conclusions: - continuous proof: This is standard, see Mac Lane, Ch. V, Theorem 5.1. @@ -11,13 +9,14 @@ - id: saft assumptions: - continuous - source_assumptions: - - cogenerating set - - complete - - locally small - - well-powered - target_assumptions: - - locally small + mapped_assumptions: + source: + - cogenerating set + - complete + - locally small + - well-powered + target: + - locally small conclusions: - right adjoint proof: This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the nLab, or in Mac Lane, Ch. V, Theorem 8.2. diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml index 27b770b0..292b812d 100644 --- a/databases/catdat/data/functor-implications/equivalences.yaml +++ b/databases/catdat/data/functor-implications/equivalences.yaml @@ -3,8 +3,6 @@ - essentially surjective - faithful - full - source_assumptions: [] - target_assumptions: [] conclusions: - equivalence proof: This is standard, see Mac Lane, Ch. IV, Theorem 4.1. @@ -13,8 +11,6 @@ - id: equivalence_consequences assumptions: - equivalence - source_assumptions: [] - target_assumptions: [] conclusions: - monadic proof: This is easy. diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml index 63bf1d37..ee9b91ea 100644 --- a/databases/catdat/data/functor-implications/limits preservation.yaml +++ b/databases/catdat/data/functor-implications/limits preservation.yaml @@ -1,8 +1,6 @@ - id: continuous_consequences assumptions: - continuous - source_assumptions: [] - target_assumptions: [] conclusions: - cofinitary - preserves products @@ -13,8 +11,6 @@ - id: products_consequences assumptions: - preserves products - source_assumptions: [] - target_assumptions: [] conclusions: - preserves finite products proof: This is trivial. @@ -23,8 +19,6 @@ - id: finite_products_consequences assumptions: - preserves finite products - source_assumptions: [] - target_assumptions: [] conclusions: - preserves terminal objects proof: This is trivial. @@ -34,9 +28,9 @@ assumptions: - preserves equalizers - preserves products - source_assumptions: - - products - target_assumptions: [] + mapped_assumptions: + source: + - products conclusions: - continuous proof: This follows from the construction of limits via equalizers and products, see Mac Lane, Ch. V, Theorem 2.2. @@ -46,9 +40,9 @@ assumptions: - cofinitary - left exact - source_assumptions: - - finitely complete - target_assumptions: [] + mapped_assumptions: + source: + - finitely complete conclusions: - continuous proof: This is because every limit can be written as a filtered limit of finite limits, see Mac Lane, Ch. IX, Theorem 1.1. @@ -58,9 +52,9 @@ assumptions: - cofinitary - preserves finite products - source_assumptions: - - finite products - target_assumptions: [] + mapped_assumptions: + source: + - finite products conclusions: - preserves products proof: This is because every product can be written as a filtered limit of finite products, see Mac Lane, Ch. IX, Theorem 1.1. @@ -69,8 +63,6 @@ - id: exact_definition assumptions: - exact - source_assumptions: [] - target_assumptions: [] conclusions: - left exact - right exact @@ -80,8 +72,6 @@ - id: left_exact_consequences assumptions: - left exact - source_assumptions: [] - target_assumptions: [] conclusions: - preserves finite products - preserves equalizers @@ -96,9 +86,9 @@ assumptions: - preserves equalizers - preserves finite products - source_assumptions: - - finite products - target_assumptions: [] + mapped_assumptions: + source: + - finite products conclusions: - left exact proof: This follows from the construction of finite limits via equalizers and finite products, see Mac Lane, Ch. V, Theorem 2.2. @@ -107,8 +97,6 @@ - id: representable_is_continuous assumptions: - representable - source_assumptions: [] - target_assumptions: [] conclusions: - continuous proof: This is standard, see Mac Lane, Ch. V, Theorem 4.1. @@ -117,8 +105,6 @@ - id: equalizers_include_coreflexive_equalizers assumptions: - preserves equalizers - source_assumptions: [] - target_assumptions: [] conclusions: - preserves coreflexive equalizers proof: This is trivial. @@ -128,9 +114,9 @@ assumptions: - preserves coreflexive equalizers - preserves finite products # TODO: only need binary products - source_assumptions: - - binary products - target_assumptions: [] + mapped_assumptions: + source: + - binary products conclusions: - preserves equalizers proof: This follows easily from this result about categories. @@ -139,9 +125,9 @@ - id: mono-preserving_criterion assumptions: - preserves equalizers - source_assumptions: - - mono-regular - target_assumptions: [] + mapped_assumptions: + source: + - mono-regular conclusions: - preserves monomorphisms proof: Any monomorphism in the domain is a regular monomorphism and is mapped to a regular monomorphism. diff --git a/databases/catdat/data/functor-implications/misc.yaml b/databases/catdat/data/functor-implications/misc.yaml index 3b714006..275a0138 100644 --- a/databases/catdat/data/functor-implications/misc.yaml +++ b/databases/catdat/data/functor-implications/misc.yaml @@ -2,9 +2,9 @@ assumptions: - conservative - preserves equalizers - source_assumptions: - - equalizers - target_assumptions: [] + mapped_assumptions: + source: + - equalizers conclusions: - faithful proof: 'Let $f,g : X \rightrightarrows Y$ be two morphisms in the source category, and choose an equalizer $E \hookrightarrow X$. By assumption, $F(E) \to F(X)$ is the equalizer of $F(f),F(g) : F(X) \rightrightarrows F(Y)$. Thus, if $F(f) = F(g)$, then $F(E) \to F(X)$ is an isomorphism. Since $F$ is conservative, $E \to X$ is an isomorphism, which means $f = g$.' @@ -14,8 +14,6 @@ assumptions: - full - faithful - source_assumptions: [] - target_assumptions: [] conclusions: - conservative proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$. diff --git a/databases/catdat/data/functor-implications/monadic.yaml b/databases/catdat/data/functor-implications/monadic.yaml index b5672a55..c6bab855 100644 --- a/databases/catdat/data/functor-implications/monadic.yaml +++ b/databases/catdat/data/functor-implications/monadic.yaml @@ -1,8 +1,6 @@ - id: monadic_consequences assumptions: - monadic - source_assumptions: [] - target_assumptions: [] conclusions: - conservative - faithful @@ -15,8 +13,9 @@ - right adjoint - conservative - preserves reflexive coequalizers - source_assumptions: - - reflexive coequalizers + mapped_assumptions: + source: + - reflexive coequalizers target_assumptions: [] conclusions: - monadic diff --git a/databases/catdat/data/functors/abelianization.yaml b/databases/catdat/data/functors/abelianization.yaml index ab54c2b0..d8b6e242 100644 --- a/databases/catdat/data/functors/abelianization.yaml +++ b/databases/catdat/data/functors/abelianization.yaml @@ -10,7 +10,7 @@ tags: - algebra - free -related_functors: [] +related: [] satisfied_properties: - property: left adjoint diff --git a/databases/catdat/data/functors/continuous-functions.yaml b/databases/catdat/data/functors/continuous-functions.yaml index 3be7f3f9..1882adc9 100644 --- a/databases/catdat/data/functors/continuous-functions.yaml +++ b/databases/catdat/data/functors/continuous-functions.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - topology -related_functors: [] +related: [] satisfied_properties: - property: continuous diff --git a/databases/catdat/data/functors/coproduct_sets.yaml b/databases/catdat/data/functors/coproduct_sets.yaml index 85b54ac0..effbabc4 100644 --- a/databases/catdat/data/functors/coproduct_sets.yaml +++ b/databases/catdat/data/functors/coproduct_sets.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - set theory -related_functors: +related: - doubling_sets - product_sets diff --git a/databases/catdat/data/functors/countable_copower_sets.yaml b/databases/catdat/data/functors/countable_copower_sets.yaml index 5e88a627..800f51a6 100644 --- a/databases/catdat/data/functors/countable_copower_sets.yaml +++ b/databases/catdat/data/functors/countable_copower_sets.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - set theory -related_functors: +related: - id_Set - coproduct_sets - doubling_sets diff --git a/databases/catdat/data/functors/diagonal_sets.yaml b/databases/catdat/data/functors/diagonal_sets.yaml index a5d27176..5448fe2b 100644 --- a/databases/catdat/data/functors/diagonal_sets.yaml +++ b/databases/catdat/data/functors/diagonal_sets.yaml @@ -10,7 +10,7 @@ left_adjoint: coproduct_sets tags: - set theory -related_functors: +related: - id_Set satisfied_properties: diff --git a/databases/catdat/data/functors/discrete_topology.yaml b/databases/catdat/data/functors/discrete_topology.yaml index ac1af518..e2f3446c 100644 --- a/databases/catdat/data/functors/discrete_topology.yaml +++ b/databases/catdat/data/functors/discrete_topology.yaml @@ -10,7 +10,7 @@ tags: - topology - free -related_functors: [] +related: [] satisfied_properties: - property: left adjoint diff --git a/databases/catdat/data/functors/doubling_sets.yaml b/databases/catdat/data/functors/doubling_sets.yaml index b9a44356..23b82344 100644 --- a/databases/catdat/data/functors/doubling_sets.yaml +++ b/databases/catdat/data/functors/doubling_sets.yaml @@ -9,7 +9,7 @@ nlab_link: null tags: - set theory -related_functors: +related: - id_Set - coproduct_sets - countable_copower_sets diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml index 45812add..1b327186 100644 --- a/databases/catdat/data/functors/enveloping_group.yaml +++ b/databases/catdat/data/functors/enveloping_group.yaml @@ -10,7 +10,7 @@ tags: - algebra - free -related_functors: +related: - free_group satisfied_properties: diff --git a/databases/catdat/data/functors/forget_abelian.yaml b/databases/catdat/data/functors/forget_abelian.yaml index d834a8a8..25561044 100644 --- a/databases/catdat/data/functors/forget_abelian.yaml +++ b/databases/catdat/data/functors/forget_abelian.yaml @@ -11,7 +11,7 @@ tags: - algebra - forgetful -related_functors: +related: - forget_group - forget_inverses diff --git a/databases/catdat/data/functors/forget_group.yaml b/databases/catdat/data/functors/forget_group.yaml index a7f2c470..081723b0 100644 --- a/databases/catdat/data/functors/forget_group.yaml +++ b/databases/catdat/data/functors/forget_group.yaml @@ -11,7 +11,7 @@ tags: - algebra - forgetful -related_functors: +related: - forget_vector - forget_ring - forget_abelian diff --git a/databases/catdat/data/functors/forget_inverses.yaml b/databases/catdat/data/functors/forget_inverses.yaml index 468c8f1c..9fc30139 100644 --- a/databases/catdat/data/functors/forget_inverses.yaml +++ b/databases/catdat/data/functors/forget_inverses.yaml @@ -11,7 +11,7 @@ tags: - algebra - forgetful -related_functors: +related: - forget_abelian satisfied_properties: diff --git a/databases/catdat/data/functors/forget_ring.yaml b/databases/catdat/data/functors/forget_ring.yaml index ae0d2995..8b05a0f3 100644 --- a/databases/catdat/data/functors/forget_ring.yaml +++ b/databases/catdat/data/functors/forget_ring.yaml @@ -10,7 +10,7 @@ tags: - algebra - forgetful -related_functors: +related: - forget_group - forget_vector diff --git a/databases/catdat/data/functors/forget_topology.yaml b/databases/catdat/data/functors/forget_topology.yaml index 54f56a48..fd49ca5d 100644 --- a/databases/catdat/data/functors/forget_topology.yaml +++ b/databases/catdat/data/functors/forget_topology.yaml @@ -11,7 +11,7 @@ tags: - topology - forgetful -related_functors: [] +related: [] satisfied_properties: - property: faithful diff --git a/databases/catdat/data/functors/forget_vector.yaml b/databases/catdat/data/functors/forget_vector.yaml index e90d4f75..674e2324 100644 --- a/databases/catdat/data/functors/forget_vector.yaml +++ b/databases/catdat/data/functors/forget_vector.yaml @@ -10,7 +10,7 @@ tags: - algebra - forgetful -related_functors: +related: - forget_group - forget_ring diff --git a/databases/catdat/data/functors/free_group.yaml b/databases/catdat/data/functors/free_group.yaml index 647889b7..461d60d5 100644 --- a/databases/catdat/data/functors/free_group.yaml +++ b/databases/catdat/data/functors/free_group.yaml @@ -10,7 +10,7 @@ tags: - algebra - free -related_functors: [] +related: [] satisfied_properties: - property: left adjoint diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml index 04c83b07..88db4e0b 100644 --- a/databases/catdat/data/functors/group_units.yaml +++ b/databases/catdat/data/functors/group_units.yaml @@ -10,7 +10,7 @@ left_adjoint: forget_inverses tags: - algebra -related_functors: [] +related: [] satisfied_properties: - property: essentially surjective diff --git a/databases/catdat/data/functors/id_Set.yaml b/databases/catdat/data/functors/id_Set.yaml index da436972..f563c4c9 100644 --- a/databases/catdat/data/functors/id_Set.yaml +++ b/databases/catdat/data/functors/id_Set.yaml @@ -10,7 +10,7 @@ left_adjoint: id_Set tags: - set theory -related_functors: +related: - squaring_sets - doubling_sets - diagonal_sets diff --git a/databases/catdat/data/functors/modulo-p.yaml b/databases/catdat/data/functors/modulo-p.yaml index 075d049c..d67c4290 100644 --- a/databases/catdat/data/functors/modulo-p.yaml +++ b/databases/catdat/data/functors/modulo-p.yaml @@ -10,7 +10,7 @@ tags: - algebra - free -related_functors: [] +related: [] satisfied_properties: - property: left adjoint diff --git a/databases/catdat/data/functors/p-torsion.yaml b/databases/catdat/data/functors/p-torsion.yaml index 8e8d869b..7ed3bdf7 100644 --- a/databases/catdat/data/functors/p-torsion.yaml +++ b/databases/catdat/data/functors/p-torsion.yaml @@ -13,7 +13,7 @@ left_adjoint: modulo-p tags: - algebra -related_functors: +related: - torsion satisfied_properties: diff --git a/databases/catdat/data/functors/power_set_contravariant.yaml b/databases/catdat/data/functors/power_set_contravariant.yaml index 207c7a04..7f643244 100644 --- a/databases/catdat/data/functors/power_set_contravariant.yaml +++ b/databases/catdat/data/functors/power_set_contravariant.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/power+set tags: - set theory -related_functors: +related: - power_set_covariant satisfied_properties: diff --git a/databases/catdat/data/functors/power_set_covariant.yaml b/databases/catdat/data/functors/power_set_covariant.yaml index 5b7c6bda..a0c9839a 100644 --- a/databases/catdat/data/functors/power_set_covariant.yaml +++ b/databases/catdat/data/functors/power_set_covariant.yaml @@ -9,7 +9,7 @@ nlab_link: https://ncatlab.org/nlab/show/power+set tags: - set theory -related_functors: +related: - power_set_contravariant satisfied_properties: diff --git a/databases/catdat/data/functors/product_sets.yaml b/databases/catdat/data/functors/product_sets.yaml index 021f049b..2d86311a 100644 --- a/databases/catdat/data/functors/product_sets.yaml +++ b/databases/catdat/data/functors/product_sets.yaml @@ -10,7 +10,7 @@ left_adjoint: diagonal_sets tags: - set theory -related_functors: +related: - squaring_sets - coproduct_sets diff --git a/databases/catdat/data/functors/sequences_sets.yaml b/databases/catdat/data/functors/sequences_sets.yaml index aafadd38..c238381f 100644 --- a/databases/catdat/data/functors/sequences_sets.yaml +++ b/databases/catdat/data/functors/sequences_sets.yaml @@ -10,7 +10,7 @@ left_adjoint: countable_copower_sets tags: - set theory -related_functors: +related: - id_Set - product_sets - squaring_sets diff --git a/databases/catdat/data/functors/squaring_sets.yaml b/databases/catdat/data/functors/squaring_sets.yaml index db900403..ea39fed0 100644 --- a/databases/catdat/data/functors/squaring_sets.yaml +++ b/databases/catdat/data/functors/squaring_sets.yaml @@ -10,7 +10,7 @@ left_adjoint: doubling_sets tags: - set theory -related_functors: +related: - id_Set - product_sets - sequences_sets diff --git a/databases/catdat/data/functors/torsion.yaml b/databases/catdat/data/functors/torsion.yaml index 76a48dd3..de975806 100644 --- a/databases/catdat/data/functors/torsion.yaml +++ b/databases/catdat/data/functors/torsion.yaml @@ -10,7 +10,7 @@ nlab_link: https://ncatlab.org/nlab/show/torsion+subgroup tags: - algebra -related_functors: +related: - p-torsion satisfied_properties: diff --git a/databases/catdat/schema/001_structures.sql b/databases/catdat/schema/001_structures.sql new file mode 100644 index 00000000..662a9b68 --- /dev/null +++ b/databases/catdat/schema/001_structures.sql @@ -0,0 +1,233 @@ +-- STRUCTURE TYPES + +CREATE TABLE structure_types ( + type TEXT PRIMARY KEY +); + +INSERT INTO structure_types (type) VALUES ('category'), ('functor'); + +-- STRUCTURES + +CREATE TABLE structures ( + id TEXT NOT NULL, + type TEXT NOT NULL, + name TEXT NOT NULL, + notation TEXT NOT NULL, + description TEXT, + nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), + PRIMARY KEY (id, type), + UNIQUE (name, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT +); + +CREATE UNIQUE INDEX idx_structures_lower_id_unique ON structures (lower(id), type); + +CREATE INDEX idx_structures_by_type ON structures (type); + +-- STRUCTURE MAPS + +CREATE TABLE structure_maps ( + map TEXT NOT NULL, + input_type TEXT NOT NULL, + output_type TEXT NOT NULL, + PRIMARY KEY (map, input_type, output_type), + FOREIGN KEY (input_type) REFERENCES structure_types (type) ON DELETE RESTRICT, + FOREIGN KEY (output_type) REFERENCES structure_types (type) ON DELETE RESTRICT +); + +INSERT INTO structure_maps (map, input_type, output_type) VALUES + ('source', 'functor', 'category'), + ('target', 'functor', 'category'), + ('left_adjoint', 'functor', 'functor'); + +CREATE TABLE structure_map_values ( + map TEXT NOT NULL, + input TEXT NOT NULL, + input_type TEXT NOT NULL, + output TEXT NOT NULL, + output_type TEXT NOT NULL, + PRIMARY KEY (map, input, input_type, output, output_type), + FOREIGN KEY (map, input_type, output_type) + REFERENCES structure_maps (map, input_type, output_type) ON DELETE CASCADE, + FOREIGN KEY (input, input_type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (output, output_type) REFERENCES structures (id, type) ON DELETE CASCADE +); + +-- TAGS + +CREATE TABLE tags ( + id INTEGER PRIMARY KEY, + tag TEXT NOT NULL, + type TEXT NOT NULL, + UNIQUE (tag, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT +); + +CREATE INDEX idx_tags_by_type ON tags (type); + +CREATE TABLE tag_assignments ( + structure TEXT NOT NULL, + tag TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (structure, tag), + FOREIGN KEY (structure, type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (tag, type) REFERENCES tags (tag, type) ON DELETE CASCADE +); + +-- RELATED AND DUAL STRUCTURES + +CREATE TABLE related_structures ( + structure TEXT NOT NULL, + related_structure TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (structure, related_structure, type), + FOREIGN KEY (structure, type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (related_structure, type) REFERENCES structures (id, type) ON DELETE CASCADE +); + +CREATE TABLE dual_structures ( + structure TEXT NOT NULL, + dual_structure TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (structure, dual_structure, type), + FOREIGN KEY (structure, type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (dual_structure, type) REFERENCES structures (id, type) ON DELETE CASCADE, + UNIQUE (structure), + UNIQUE (dual_structure) +); + +-- COMMENTS + +CREATE TABLE structure_comments ( + id INTEGER PRIMARY KEY, + structure TEXT NOT NULL, + type TEXT NOT NULL, + comment TEXT NOT NULL, + FOREIGN KEY (structure, type) REFERENCES structures (id, type) ON DELETE CASCADE +); + +CREATE INDEX idx_comments_by_structure ON structure_comments (structure, type); + +-- PROPERTIES OF STRUCTURES + +CREATE TABLE relations ( + relation TEXT PRIMARY KEY, + conditional TEXT NOT NULL +); + +CREATE TABLE properties ( + id TEXT NOT NULL, + type TEXT NOT NULL, + relation TEXT NOT NULL, + description TEXT NOT NULL CHECK (length(description) > 0), + nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), + invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE, + CHECK (invariant_under_equivalences in (TRUE, FALSE)), + PRIMARY KEY (id, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, + FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT +); + +CREATE UNIQUE INDEX idx_properties_lower_id_unique ON properties (lower(id), type); + +CREATE INDEX idx_properties_by_type ON properties (type); + +-- RELATED AND DUAL PROPERTIES + +CREATE TABLE related_properties ( + property TEXT NOT NULL, + related_property TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (property, related_property, type), + FOREIGN KEY (property, type) REFERENCES properties (id, type) ON DELETE CASCADE, + FOREIGN KEY (related_property, type) REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE TABLE dual_properties ( + property TEXT NOT NULL, + dual_property TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (property, dual_property, type), + FOREIGN KEY (property, type) REFERENCES properties (id, type) ON DELETE CASCADE, + FOREIGN KEY (dual_property, type) REFERENCES properties (id, type) ON DELETE CASCADE, + UNIQUE (property, type), + UNIQUE (dual_property, type) +); + +-- PROPERTY ASSIGNMENTS + +CREATE TABLE property_assignments ( + id INTEGER PRIMARY KEY, + type TEXT NOT NULL, + structure TEXT NOT NULL, + property TEXT NOT NULL, + is_satisfied INTEGER + -- we use is_satisfied = NULL for undecidable properties + CHECK (is_satisfied in (TRUE, FALSE, NULL)), + proof TEXT NOT NULL CHECK (length(proof) > 0), + is_deduced INTEGER NOT NULL DEFAULT FALSE + CHECK (is_deduced in (TRUE, FALSE)), + check_redundancy INTEGER NOT NULL DEFAULT TRUE + CHECK (check_redundancy in (TRUE, FALSE)), + UNIQUE (structure, property, type), + FOREIGN KEY (structure, type) REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (property, type) REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE INDEX idx_assignment_by_property ON property_assignments (property, type); +CREATE INDEX idx_assignment_by_type ON property_assignments (type); + +-- IMPLICATIONS BETWEEN PROPERTIES + +CREATE TABLE implications ( + id TEXT NOT NULL, + type TEXT NOT NULL, + proof TEXT NOT NULL CHECK (length(proof) > 0), + is_equivalence INTEGER NOT NULL DEFAULT FALSE + CHECK (is_equivalence in (TRUE, FALSE)), + is_deduced INTEGER NOT NULL DEFAULT FALSE + CHECK (is_deduced in (TRUE, FALSE)), + dualized_from TEXT, + CHECK (dualized_from IS NULL OR is_deduced = TRUE), + PRIMARY KEY (id, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, + FOREIGN KEY (dualized_from, type) REFERENCES implications (id, type) ON DELETE CASCADE +); + +CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id), type); + +CREATE TABLE assumptions ( + implication TEXT NOT NULL, + property TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (implication, property, type), + FOREIGN KEY (implication, type) REFERENCES implications (id, type) ON DELETE CASCADE, + FOREIGN KEY (property, type) REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE TABLE conclusions ( + implication TEXT NOT NULL, + property TEXT NOT NULL, + type TEXT NOT NULL, + PRIMARY KEY (implication, property, type), + FOREIGN KEY (implication, type) REFERENCES implications (id, type) ON DELETE CASCADE, + FOREIGN KEY (property, type) REFERENCES properties (id, type) ON DELETE CASCADE +); + +CREATE TABLE mapped_assumptions ( + map TEXT NOT NULL, + implication TEXT NOT NULL, + implication_type TEXT NOT NULL, + property TEXT NOT NULL, + property_type TEXT NOT NULL, + PRIMARY KEY (map, implication, implication_type, property, property_type), + FOREIGN KEY (implication, implication_type) + REFERENCES implications (id, type) + ON DELETE CASCADE, + FOREIGN KEY (property, property_type) + REFERENCES properties (id, type) + ON DELETE CASCADE, + FOREIGN KEY (map, implication_type, property_type) + REFERENCES structure_maps (map, input_type, output_type) + ON DELETE CASCADE +); \ No newline at end of file diff --git a/databases/catdat/schema/001_tags.sql b/databases/catdat/schema/001_tags.sql deleted file mode 100644 index 544a385d..00000000 --- a/databases/catdat/schema/001_tags.sql +++ /dev/null @@ -1,9 +0,0 @@ -CREATE TABLE category_tags ( - id INTEGER PRIMARY KEY, - tag TEXT NOT NULL UNIQUE -); - -CREATE TABLE functor_tags ( - id INTEGER PRIMARY KEY, - tag TEXT NOT NULL UNIQUE -); \ No newline at end of file diff --git a/databases/catdat/schema/002_categories.sql b/databases/catdat/schema/002_categories.sql new file mode 100644 index 00000000..b2feebdc --- /dev/null +++ b/databases/catdat/schema/002_categories.sql @@ -0,0 +1,53 @@ +CREATE TABLE categories ( + id TEXT PRIMARY KEY, + type NOT NULL DEFAULT 'category' CHECK (type = 'category'), + objects TEXT NOT NULL, + morphisms TEXT NOT NULL, + FOREIGN KEY (id, type) REFERENCES structures (id, type) ON DELETE CASCADE +); + +CREATE VIEW categories_view AS + SELECT + s.id, s.name, s.notation, s.description, s.nlab_link, + c.objects, c.morphisms, d.dual_structure as dual_category + FROM categories c + INNER JOIN structures s ON s.id = c.id + LEFT JOIN dual_structures d ON d.structure = c.id AND d.type = c.type +; + +CREATE TABLE special_object_types ( + id INTEGER PRIMARY KEY, + type TEXT NOT NULL UNIQUE, + dual TEXT, + FOREIGN KEY (dual) REFERENCES special_object_types (type) ON DELETE SET NULL +); + +CREATE TABLE special_objects ( + category TEXT NOT NULL, + type TEXT NOT NULL, + description TEXT NOT NULL, + PRIMARY KEY (category, type), + FOREIGN KEY (type) REFERENCES special_object_types (type) ON DELETE RESTRICT, + FOREIGN KEY (category) REFERENCES categories (id) ON DELETE CASCADE +); + +CREATE INDEX idx_special_objects_by_category ON special_objects (category); + +CREATE TABLE special_morphism_types ( + id INTEGER PRIMARY KEY, + type TEXT NOT NULL UNIQUE, + dual TEXT, + FOREIGN KEY (dual) REFERENCES special_morphism_types (type) ON DELETE SET NULL +); + +CREATE TABLE special_morphisms ( + category TEXT NOT NULL, + type TEXT NOT NULL, + description TEXT NOT NULL, + proof TEXT NOT NULL, + PRIMARY KEY (category, type), + FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT, + FOREIGN KEY (category) REFERENCES categories (id) ON DELETE CASCADE +); + +CREATE INDEX idx_special_morphisms_by_category ON special_morphisms (category); \ No newline at end of file diff --git a/databases/catdat/schema/002_relations.sql b/databases/catdat/schema/002_relations.sql deleted file mode 100644 index e49f4709..00000000 --- a/databases/catdat/schema/002_relations.sql +++ /dev/null @@ -1,4 +0,0 @@ -CREATE TABLE relations ( - relation TEXT PRIMARY KEY, - conditional TEXT NOT NULL -); \ No newline at end of file diff --git a/databases/catdat/schema/003_categories.sql b/databases/catdat/schema/003_categories.sql deleted file mode 100644 index 87ec2192..00000000 --- a/databases/catdat/schema/003_categories.sql +++ /dev/null @@ -1,39 +0,0 @@ -CREATE TABLE categories ( - id TEXT PRIMARY KEY, - name TEXT NOT NULL UNIQUE, - notation TEXT NOT NULL, - objects TEXT NOT NULL, - morphisms TEXT NOT NULL, - description TEXT, - nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), - dual_category_id TEXT REFERENCES categories (id) -); - -CREATE UNIQUE INDEX categories_lower_id_unique ON categories (lower(id)); - -CREATE TABLE category_tag_assignments ( - category_id TEXT NOT NULL, - tag TEXT NOT NULL, - PRIMARY KEY (category_id, tag), - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (tag) REFERENCES category_tags (tag) ON DELETE CASCADE -); - -CREATE TABLE related_categories ( - category_id TEXT NOT NULL, - related_category_id TEXT NOT NULL, - PRIMARY KEY (category_id, related_category_id), - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (related_category_id) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE TABLE category_comments ( - id INTEGER PRIMARY KEY, - category_id TEXT NOT NULL, - comment TEXT NOT NULL, - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE INDEX idx_category_comments ON category_comments (category_id); - - diff --git a/databases/catdat/schema/004_category-properties.sql b/databases/catdat/schema/004_category-properties.sql deleted file mode 100644 index 9604ad82..00000000 --- a/databases/catdat/schema/004_category-properties.sql +++ /dev/null @@ -1,39 +0,0 @@ -CREATE TABLE category_properties ( - id TEXT PRIMARY KEY, - relation TEXT NOT NULL, - description TEXT NOT NULL CHECK (length(description) > 0), - nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), - invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE, - dual_property_id TEXT, - FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT, - FOREIGN KEY (dual_property_id) REFERENCES category_properties (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX category_properties_lower_id_unique ON category_properties (lower(id)); - -CREATE TABLE related_category_properties ( - property_id TEXT NOT NULL, - related_property_id TEXT NOT NULL, - PRIMARY KEY (property_id, related_property_id), - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE, - FOREIGN KEY (related_property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE TABLE category_property_assignments ( - id INTEGER PRIMARY KEY, - category_id TEXT NOT NULL, - property_id TEXT NOT NULL, - is_satisfied INTEGER - -- we use NULL for undecidable properties - CHECK (is_satisfied in (TRUE, FALSE, NULL)), - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_deduced INTEGER NOT NULL DEFAULT FALSE - CHECK (is_deduced in (TRUE, FALSE)), - check_redundancy INTEGER NOT NULL DEFAULT TRUE - CHECK (check_redundancy in (TRUE, FALSE)), - UNIQUE (category_id, property_id), - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE INDEX idx_property_category ON category_property_assignments (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/005_category-implications.sql b/databases/catdat/schema/005_category-implications.sql deleted file mode 100644 index 52d81ea0..00000000 --- a/databases/catdat/schema/005_category-implications.sql +++ /dev/null @@ -1,31 +0,0 @@ -CREATE TABLE category_implications ( - id TEXT PRIMARY KEY, - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_equivalence INTEGER NOT NULL DEFAULT FALSE, - is_deduced INTEGER NOT NULL DEFAULT FALSE, - dualized_from TEXT, - CHECK (dualized_from IS NULL OR is_deduced = TRUE), - FOREIGN KEY (dualized_from) REFERENCES category_implications (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX category_implications_lower_id_unique ON category_implications (lower(id)); - -CREATE TABLE category_implication_assumptions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES category_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE TABLE category_implication_conclusions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES category_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE INDEX idx_assumptions_category_property ON category_implication_assumptions (property_id); - -CREATE INDEX idx_conclusions_category_property ON category_implication_conclusions (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/006_category-implications-view.sql b/databases/catdat/schema/006_category-implications-view.sql deleted file mode 100644 index 7f60eb25..00000000 --- a/databases/catdat/schema/006_category-implications-view.sql +++ /dev/null @@ -1,47 +0,0 @@ -CREATE VIEW category_implications_view AS -SELECT - i.id, - i.is_equivalence, - i.proof, - i.is_deduced, - i.dualized_from, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_implication_assumptions a - WHERE a.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS assumptions, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_implication_conclusions c - WHERE c.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS conclusions -FROM category_implications i; - - -CREATE TRIGGER trg_category_implications_view_insert -INSTEAD OF INSERT ON category_implications_view -BEGIN - INSERT INTO category_implications - (id, is_equivalence, proof, is_deduced, dualized_from) - VALUES ( - NEW.id, - COALESCE(NEW.is_equivalence, FALSE), - NEW.proof, - COALESCE(NEW.is_deduced, FALSE), - NEW.dualized_from - ); - - INSERT INTO category_implication_assumptions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.assumptions); - - INSERT INTO category_implication_conclusions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.conclusions); -END; \ No newline at end of file diff --git a/databases/catdat/schema/007_special_objects.sql b/databases/catdat/schema/007_special_objects.sql deleted file mode 100644 index 71aff7b4..00000000 --- a/databases/catdat/schema/007_special_objects.sql +++ /dev/null @@ -1,17 +0,0 @@ -CREATE TABLE special_object_types ( - id INTEGER PRIMARY KEY, - type TEXT NOT NULL UNIQUE, - dual TEXT, - FOREIGN KEY (dual) REFERENCES special_object_types (type) ON DELETE SET NULL -); - -CREATE TABLE special_objects ( - category_id TEXT NOT NULL, - type TEXT NOT NULL, - description TEXT NOT NULL, - PRIMARY KEY (category_id, type), - FOREIGN KEY (type) REFERENCES special_object_types (type) ON DELETE RESTRICT, - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE INDEX idx_special_objects_by_category ON special_objects (category_id); \ No newline at end of file diff --git a/databases/catdat/schema/008_special-morphisms.sql b/databases/catdat/schema/008_special-morphisms.sql deleted file mode 100644 index 022e3955..00000000 --- a/databases/catdat/schema/008_special-morphisms.sql +++ /dev/null @@ -1,18 +0,0 @@ -CREATE TABLE special_morphism_types ( - id INTEGER PRIMARY KEY, - type TEXT NOT NULL UNIQUE, - dual TEXT, - FOREIGN KEY (dual) REFERENCES special_morphism_types (type) ON DELETE SET NULL -); - -CREATE TABLE special_morphisms ( - category_id TEXT NOT NULL, - type TEXT NOT NULL, - description TEXT NOT NULL, - proof TEXT NOT NULL, - PRIMARY KEY (category_id, type), - FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT, - FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE INDEX idx_special_morphisms_by_category ON special_morphisms (category_id); \ No newline at end of file diff --git a/databases/catdat/schema/009_functors.sql b/databases/catdat/schema/009_functors.sql deleted file mode 100644 index 418c3b6f..00000000 --- a/databases/catdat/schema/009_functors.sql +++ /dev/null @@ -1,38 +0,0 @@ -CREATE TABLE functors ( - id TEXT PRIMARY KEY, - name TEXT NOT NULL UNIQUE, - notation TEXT NOT NULL, - source TEXT NOT NULL, - target TEXT NOT NULL, - description TEXT NOT NULL CHECK (length(description) > 0), - nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), - FOREIGN KEY (source) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (target) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE UNIQUE INDEX functors_lower_id_unique ON functors (lower(id)); - -CREATE TABLE functor_tag_assignments ( - functor_id TEXT NOT NULL, - tag TEXT NOT NULL, - PRIMARY KEY (functor_id, tag), - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (tag) REFERENCES functor_tags (tag) ON DELETE CASCADE -); - -CREATE TABLE related_functors ( - functor_id TEXT NOT NULL, - related_functor_id TEXT NOT NULL, - PRIMARY KEY (functor_id, related_functor_id), - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (related_functor_id) REFERENCES functors (id) ON DELETE CASCADE -); - -CREATE TABLE functor_comments ( - id INTEGER PRIMARY KEY, - functor_id TEXT NOT NULL, - comment TEXT NOT NULL, - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE -); - -CREATE INDEX idx_functor_comments ON functor_comments (functor_id); diff --git a/databases/catdat/schema/010_functor-properties.sql b/databases/catdat/schema/010_functor-properties.sql deleted file mode 100644 index f1dbec5d..00000000 --- a/databases/catdat/schema/010_functor-properties.sql +++ /dev/null @@ -1,51 +0,0 @@ -CREATE TABLE functor_properties ( - id TEXT PRIMARY KEY, - relation TEXT NOT NULL, - description TEXT NOT NULL CHECK (length(description) > 0), - nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), - invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE, - dual_property_id TEXT, - required_source TEXT, - required_target TEXT, - FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT, - FOREIGN KEY (dual_property_id) REFERENCES functor_properties (id) ON DELETE SET NULL, - FOREIGN KEY (required_source) REFERENCES categories (id) ON DELETE SET NULL, - FOREIGN KEY (required_target) REFERENCES categories (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX functor_properties_lower_id_unique ON functor_properties (lower(id)); - -CREATE INDEX idx_functor_properties_required_source -ON functor_properties(required_source) -WHERE required_source IS NOT NULL; - -CREATE INDEX idx_functor_properties_required_target -ON functor_properties(required_target) -WHERE required_target IS NOT NULL; - -CREATE TABLE related_functor_properties ( - property_id TEXT NOT NULL, - related_property_id TEXT NOT NULL, - PRIMARY KEY (property_id, related_property_id), - FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE, - FOREIGN KEY (related_property_id) REFERENCES functor_properties (id) ON DELETE CASCADE -); - -CREATE TABLE functor_property_assignments ( - id INTEGER PRIMARY KEY, - functor_id TEXT NOT NULL, - property_id TEXT NOT NULL, - is_satisfied INTEGER - -- we use NULL for undecidable properties - CHECK (is_satisfied in (TRUE, FALSE, NULL)), - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_deduced INTEGER NOT NULL DEFAULT FALSE - CHECK (is_deduced in (TRUE, FALSE)), - check_redundancy INTEGER NOT NULL DEFAULT TRUE - CHECK (check_redundancy in (TRUE, FALSE)), - UNIQUE (functor_id, property_id), - FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE -); - -CREATE INDEX idx_property_functor ON functor_property_assignments (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/011_functor-implications.sql b/databases/catdat/schema/011_functor-implications.sql deleted file mode 100644 index 9d505cd1..00000000 --- a/databases/catdat/schema/011_functor-implications.sql +++ /dev/null @@ -1,53 +0,0 @@ -CREATE TABLE functor_implications ( - id TEXT PRIMARY KEY, - proof TEXT NOT NULL CHECK (length(proof) > 0), - is_equivalence INTEGER NOT NULL DEFAULT FALSE, - is_deduced INTEGER NOT NULL DEFAULT FALSE, - dualized_from TEXT, - CHECK (dualized_from IS NULL OR is_deduced = TRUE), - FOREIGN KEY (dualized_from) REFERENCES functor_implications (id) ON DELETE SET NULL -); - -CREATE UNIQUE INDEX functor_implications_lower_id_unique ON functor_implications (lower(id)); - -CREATE TABLE functor_implication_assumptions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE -); - -CREATE TABLE functor_implication_conclusions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE -); - --- property of source category -CREATE TABLE functor_implication_source_assumptions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - --- property of target category -CREATE TABLE functor_implication_target_assumptions ( - implication_id TEXT NOT NULL, - property_id TEXT NOT NULL, - PRIMARY KEY (implication_id, property_id), - FOREIGN KEY (implication_id) REFERENCES functor_implications (id) ON DELETE CASCADE, - FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE -); - -CREATE INDEX idx_assumptions_functor_property ON functor_implication_assumptions (property_id); - -CREATE INDEX idx_conclusions_functor_property ON functor_implication_conclusions (property_id); - -CREATE INDEX idx_assumptions_functor_source_property ON functor_implication_source_assumptions (property_id); - -CREATE INDEX idx_conclusions_functor_target_property ON functor_implication_target_assumptions (property_id); \ No newline at end of file diff --git a/databases/catdat/schema/012_functor-implications-view.sql b/databases/catdat/schema/012_functor-implications-view.sql deleted file mode 100644 index c75256cc..00000000 --- a/databases/catdat/schema/012_functor-implications-view.sql +++ /dev/null @@ -1,71 +0,0 @@ -CREATE VIEW functor_implications_view AS -SELECT - i.id, - i.is_equivalence, - i.proof, - i.is_deduced, - i.dualized_from, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM functor_implication_assumptions a - WHERE a.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS assumptions, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM functor_implication_source_assumptions a - WHERE a.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS source_assumptions, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM functor_implication_target_assumptions a - WHERE a.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS target_assumptions, - ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM functor_implication_conclusions c - WHERE c.implication_id = i.id - ORDER BY lower(property_id) - ) - ) AS conclusions -FROM functor_implications i; - - -CREATE TRIGGER trg_functor_implications_view_insert -INSTEAD OF INSERT ON functor_implications_view -BEGIN - INSERT INTO functor_implications - (id, is_equivalence, proof, is_deduced, dualized_from) - VALUES ( - NEW.id, - COALESCE(NEW.is_equivalence, FALSE), - NEW.proof, - COALESCE(NEW.is_deduced, FALSE), - NEW.dualized_from - ); - - INSERT INTO functor_implication_assumptions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.assumptions); - - INSERT INTO functor_implication_source_assumptions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.source_assumptions); - - INSERT INTO functor_implication_target_assumptions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.target_assumptions); - - INSERT INTO functor_implication_conclusions (implication_id, property_id) - SELECT NEW.id, value - FROM json_each(NEW.conclusions); -END; \ No newline at end of file diff --git a/databases/catdat/schema/013_adjoint-functors.sql b/databases/catdat/schema/013_adjoint-functors.sql deleted file mode 100644 index dfb40a43..00000000 --- a/databases/catdat/schema/013_adjoint-functors.sql +++ /dev/null @@ -1,26 +0,0 @@ -CREATE TABLE adjoint_functors ( - left_adjoint TEXT NOT NULL, - right_adjoint TEXT NOT NULL, - PRIMARY KEY (left_adjoint, right_adjoint), - UNIQUE (left_adjoint), - UNIQUE (right_adjoint), - FOREIGN KEY (left_adjoint) REFERENCES functors (id) ON DELETE CASCADE, - FOREIGN KEY (right_adjoint) REFERENCES functors (id) ON DELETE CASCADE -); - -CREATE TRIGGER adjoint_functors_source_target_check_insert -BEFORE INSERT ON adjoint_functors -BEGIN - SELECT - CASE - WHEN ( - (SELECT source FROM functors WHERE id = NEW.left_adjoint) != - (SELECT target FROM functors WHERE id = NEW.right_adjoint) - ) - OR ( - (SELECT target FROM functors WHERE id = NEW.left_adjoint) != - (SELECT source FROM functors WHERE id = NEW.right_adjoint) - ) - THEN RAISE(ABORT, 'Adjoint functors must have reversed source/target') - END; -END; \ No newline at end of file diff --git a/databases/catdat/scripts/config.ts b/databases/catdat/scripts/config.ts index 027cdd85..da9fab63 100644 --- a/databases/catdat/scripts/config.ts +++ b/databases/catdat/scripts/config.ts @@ -1,14 +1,17 @@ export type StructureType = 'category' | 'functor' -export const STRUCTURES: StructureType[] = ['category', 'functor'] - -export const PLURALS = { - category: 'categories', - functor: 'functors', -} - /** * Proofs longer than this value raise a warning * that suggests to use content pages instead. */ export const PROOF_LENGTH_THRESHOLD = 1200 + +// TODO: remove duplication with "structure_maps" table +export const STRUCTURE_MAPS: Record> = { + category: {}, + functor: { + source: 'category', + target: 'category', + left_adjoint: 'functor', + }, +} diff --git a/databases/catdat/scripts/deduce-category-implications.ts b/databases/catdat/scripts/deduce-category-implications.ts deleted file mode 100644 index ad91c32a..00000000 --- a/databases/catdat/scripts/deduce-category-implications.ts +++ /dev/null @@ -1,117 +0,0 @@ -import { get_client } from './utils/helpers' -import { clear_deduced_implications, is_dualizable } from './utils/implications' - -const db = get_client() - -/** - * Deduces category implications from given ones. - */ -export function deduce_category_implications() { - console.info('\n--- Deduce category implications ---') - clear_deduced_implications(db, 'category') - create_dualized_category_implications() - create_self_dual_category_implications() -} - -/** - * Dualizes all implications of categories by dualizing the involved properties - * (in case they have a dual). For example, if P ===> Q holds, - * then P^op ===> Q^op holds as well. - */ -function create_dualized_category_implications() { - const implications_query = db.prepare( - `SELECT - v.id, - v.assumptions, - v.conclusions, - v.is_equivalence, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.assumptions) a - JOIN category_properties p ON p.id = a.value - ) AS dual_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.conclusions) c - JOIN category_properties p ON p.id = c.value - ) AS dual_conclusions - FROM category_implications_view v - WHERE v.is_deduced = FALSE`, - ) - - const implications = implications_query.all() as { - id: string - assumptions: string - conclusions: string - dual_assumptions: string - dual_conclusions: string - is_equivalence: 0 | 1 - }[] - - const dualizable_implications = implications.filter(is_dualizable) - - const insert_query = db.prepare( - `INSERT INTO category_implications_view ( - id, - assumptions, - conclusions, - is_equivalence, - is_deduced, - dualized_from, - proof - ) VALUES (?, ?, ?, ?, TRUE, ?, ?)`, - ) - - const insert_duals = db.transaction(() => { - for (const impl of dualizable_implications) { - insert_query.run( - `dual_${impl.id}`, - impl.dual_assumptions, - impl.dual_conclusions, - impl.is_equivalence, - impl.id, - 'This follows from the dual implication.', - ) - } - }) - - insert_duals() - - console.info(`Deduced ${dualizable_implications.length} implications by duality`) -} - -/** - * Creates all trivial implications of the form - * self-dual + P ===> P^op - */ -function create_self_dual_category_implications() { - const rows = db - .prepare( - `INSERT INTO category_implications_view ( - id, - assumptions, - conclusions, - is_equivalence, - proof, - is_deduced - ) - SELECT - 'self-dual_' || p.id, - json_array('self-dual', p.id), - json_array(p.dual_property_id), - FALSE, - 'This holds by self-duality.', - TRUE - FROM - category_properties p - WHERE - p.dual_property_id IS NOT NULL - AND p.id != 'self-dual' - AND p.id != p.dual_property_id - AND p.invariant_under_equivalences = TRUE - RETURNING id`, - ) - .all() - - console.info(`Deduced ${rows.length} implications by self-duality`) -} diff --git a/databases/catdat/scripts/deduce-functor-implications.ts b/databases/catdat/scripts/deduce-functor-implications.ts deleted file mode 100644 index 48628188..00000000 --- a/databases/catdat/scripts/deduce-functor-implications.ts +++ /dev/null @@ -1,97 +0,0 @@ -import { get_client } from './utils/helpers' -import { clear_deduced_implications, is_dualizable } from './utils/implications' - -const db = get_client() - -/** - * Deduces functor implications from given ones. - */ -export function deduce_functor_implications() { - console.info('\n--- Deduce functor implications ---') - clear_deduced_implications(db, 'functor') - create_dualized_functor_implications() -} - -/** - * Dualizes all implications of functors by dualizing the involved properties - * (in case they have a dual). For example, if P ===> Q holds, - * then P^op ===> Q^op holds as well. The assumptions of source and target - * categories (if any) need to be dualized as well. - */ -function create_dualized_functor_implications() { - const implications_query = db.prepare( - `SELECT - v.id, - v.assumptions, - v.conclusions, - v.is_equivalence, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.assumptions) a - JOIN functor_properties p ON p.id = a.value - ) AS dual_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.source_assumptions) sa - JOIN category_properties p ON p.id = sa.value - ) AS dual_source_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.target_assumptions) ta - JOIN category_properties p ON p.id = ta.value - ) AS dual_target_assumptions, - ( - SELECT json_group_array(p.dual_property_id) - FROM json_each(v.conclusions) c - JOIN functor_properties p ON p.id = c.value - ) AS dual_conclusions - FROM functor_implications_view v - WHERE v.is_deduced = FALSE`, - ) - - const implications = implications_query.all() as { - id: string - assumptions: string - conclusions: string - dual_assumptions: string - dual_source_assumptions: string - dual_target_assumptions: string - dual_conclusions: string - is_equivalence: 0 | 1 - }[] - - const dualizable_implications = implications.filter(is_dualizable) - - const insert_query = db.prepare( - `INSERT INTO functor_implications_view ( - id, - assumptions, - source_assumptions, - target_assumptions, - conclusions, - is_equivalence, - is_deduced, - dualized_from, - proof - ) VALUES (?, ?, ?, ?, ?, ?, TRUE, ?, ?)`, - ) - - const insert_duals = db.transaction(() => { - for (const impl of dualizable_implications) { - insert_query.run( - `dual_${impl.id}`, - impl.dual_assumptions, - impl.dual_source_assumptions, - impl.dual_target_assumptions, - impl.dual_conclusions, - impl.is_equivalence, - impl.id, - 'This follows from the dual implication.', - ) - } - }) - - insert_duals() - - console.info(`Deduced ${dualizable_implications.length} implications by duality`) -} diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts new file mode 100644 index 00000000..8191be42 --- /dev/null +++ b/databases/catdat/scripts/deduce-implications.ts @@ -0,0 +1,217 @@ +import { StructureType } from './config' +import { are_equal_sets, get_client } from './utils/helpers' + +const db = get_client() + +/** + * Deduces implications from given ones. + */ +export function deduce_implications() { + console.info('\n--- Deduce implications ---') + + clear_all_deduced_implications() + dualize_implications('category') + dualize_implications('functor') + create_self_dual_implications() +} + +/** + * Removes all deduced implications. + */ +function clear_all_deduced_implications() { + db.prepare(`DELETE FROM implications WHERE is_deduced = TRUE`).run() +} + +type ImplicationProperty = { + id: string + is_equivalence: 0 | 1 + kind: 'assumption' | 'conclusion' + structure: 'self' | 'source' | 'target' + property_id: string + dual_property_id: string | null +} + +type ImplicationFull = { + id: string + is_equivalence: 0 | 1 + properties: { + id: string + dual: string | null + kind: 'assumption' | 'conclusion' + structure: 'self' | 'source' | 'target' + }[] +} + +/** + * Dualizes all implications by dualizing the involved properties + * (in case they have a dual). For example, if P ===> Q holds, + * then P^op ===> Q^op holds as well. + */ +function dualize_implications(type: StructureType) { + const implication_properties_query = db.prepare<[string], ImplicationProperty>(` + SELECT + i.id, + i.is_equivalence, + ip.kind, + ip.structure, + ip.property_id, + d.dual_property_id + FROM implications i + INNER JOIN implication_properties ip + ON ip.implication_id = i.id + LEFT JOIN dual_properties d + ON d.property_id = ip.property_id + WHERE i.is_deduced = FALSE AND i.type = ? + ORDER BY i.id + `) + + const dual_implication_insert = db.prepare(` + INSERT INTO implications + (id, type, is_equivalence, is_deduced, dualized_from, proof) + VALUES (?, ?, ?, TRUE, ?, ?) + `) + + const implication_property_insert = db.prepare(` + INSERT INTO implication_properties + (implication_id, property_id, type, kind, structure) + VALUES (?, ?, ?, ?, ?) + `) + + const tx = db.transaction(() => { + const implication_properties = implication_properties_query.all(type) + const implications_dict = get_implications_dict(implication_properties) + const count = Object.values(implications_dict).length + + for (const impl of Object.values(implications_dict)) { + dual_implication_insert.run( + `dual_${impl.id}`, + type, + impl.is_equivalence, + impl.id, + 'This follows from the dual implication.', + ) + + for (const p of impl.properties) { + implication_property_insert.run( + `dual_${impl.id}`, + p.dual, + type, + p.kind, + p.structure, + ) + } + } + + console.info(`Deduced ${count} ${type} implications by duality`) + }) + + tx() +} + +/** + * Checks if all properties of an implication have a dual + * and that the dualized implication is different from the original. + */ +function is_dualizable(impl: ImplicationFull): boolean { + if (impl.properties.some((p) => !p.dual)) return false + + const kinds = new Set(impl.properties.map((p) => p.kind)) + const structures = new Set(impl.properties.map((p) => p.structure)) + + for (const kind of kinds) { + for (const structure of structures) { + const props = impl.properties.filter( + (p) => p.kind === kind && p.structure === structure, + ) + if (!props.length) continue + const prop_ids = new Set(props.map((p) => p.id)) + const dual_prop_ids = new Set(props.map((p) => p.dual)) + if (!are_equal_sets(prop_ids, dual_prop_ids)) return true + } + } + + return false +} + +function get_implications_dict( + implication_properties: ImplicationProperty[], +): Record { + const implications_dict: Record = {} + + for (const impl_prop of implication_properties) { + const { id, is_equivalence, property_id, dual_property_id, kind, structure } = + impl_prop + implications_dict[id] ??= { id, is_equivalence, properties: [] } + + implications_dict[id].properties.push({ + id: property_id, + dual: dual_property_id, + kind, + structure, + }) + } + + for (const id in implications_dict) { + if (!is_dualizable(implications_dict[id])) { + delete implications_dict[id] + } + } + + return implications_dict +} + +/** + * Creates all trivial implications of the form + * self-dual + P ===> P^op + * This is currently only applicable to properties of categories. + */ +function create_self_dual_implications() { + const properties_query = db.prepare< + never[], + { property_id: string; dual_property_id: string; type: string } + >(` + SELECT + d.property_id, + d.dual_property_id, + p.type + FROM + dual_properties d + INNER JOIN properties p + ON p.id = d.property_id + WHERE + p.invariant_under_equivalences = TRUE + AND p.id != 'self-dual' + AND p.id != d.dual_property_id + AND p.type != 'functor' + `) + + const self_dual_implication_query = db.prepare(` + INSERT INTO implications + (id, type, is_equivalence, is_deduced, proof) + VALUES (?, ?, FALSE, TRUE, 'This holds by self-duality.') + `) + + const implication_property_query = db.prepare(` + INSERT INTO implication_properties + (implication_id, property_id, type, kind, structure) + VALUES (?, ?, ?, ?, 'self') + `) + + const tx = db.transaction(() => { + const property_pairs = properties_query.all() + + for (const { property_id, dual_property_id, type } of property_pairs) { + const id = `self-dual_${property_id}` + + self_dual_implication_query.run(id, type) + + implication_property_query.run(id, 'self-dual', type, 'assumption') + implication_property_query.run(id, property_id, type, 'assumption') + implication_property_query.run(id, dual_property_id, type, 'conclusion') + } + + console.info(`Deduced ${property_pairs.length} implications by self-duality`) + }) + + tx() +} diff --git a/databases/catdat/scripts/deduce-special-morphisms.ts b/databases/catdat/scripts/deduce-special-morphisms.ts index 8e09db96..da7bfe80 100644 --- a/databases/catdat/scripts/deduce-special-morphisms.ts +++ b/databases/catdat/scripts/deduce-special-morphisms.ts @@ -18,19 +18,17 @@ export function deduce_special_morphisms() { function deduce_special_morphisms_of_dual_categories() { const res = db .prepare( - ` - INSERT INTO special_morphisms (category_id, type, description, proof) - SELECT - c.dual_category_id, - t.dual, - m.description, - 'This is deduced from its dual category.' - FROM categories c - INNER JOIN special_morphisms m ON m.category_id = c.id - INNER JOIN special_morphism_types t ON t.type = m.type - WHERE c.dual_category_id IS NOT NULL - ON CONFLICT DO NOTHING - `, + `INSERT INTO special_morphisms (category_id, type, description, proof) + SELECT + d.dual_structure_id, + t.dual, + m.description, + 'This is deduced from its dual category.' + FROM dual_structures d + INNER JOIN special_morphisms m ON m.category_id = d.structure_id + INNER JOIN special_morphism_types t ON t.type = m.type + WHERE d.type = 'category' + ON CONFLICT DO NOTHING`, ) .run() diff --git a/databases/catdat/scripts/deduce-special-objects.ts b/databases/catdat/scripts/deduce-special-objects.ts index 966f582a..09d7109f 100644 --- a/databases/catdat/scripts/deduce-special-objects.ts +++ b/databases/catdat/scripts/deduce-special-objects.ts @@ -16,13 +16,13 @@ async function deduce_special_objects_of_dual_categories() { .prepare( `INSERT INTO special_objects (category_id, type, description) SELECT - c.dual_category_id, + d.dual_structure_id, t.dual, o.description - FROM categories c - INNER JOIN special_objects o ON o.category_id = c.id + FROM dual_structures d + INNER JOIN special_objects o ON o.category_id = d.structure_id INNER JOIN special_object_types t ON t.type = o.type - WHERE c.dual_category_id IS NOT NULL + WHERE d.type = 'category' ON CONFLICT DO NOTHING`, ) .run() diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 014a27c7..5868db5b 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -7,15 +7,18 @@ import { type Database, SqliteError } from 'better-sqlite3' import { get_client, is_subset } from './utils/helpers' import { get_structures, - get_normalized_implications, get_properties_dict, get_property_assignments, is_dual_structure, type StructureMeta, - type NormalizedImplication, type PropertyMeta, } from './utils/deduction' -import { get_contradiction_string, get_proof_string } from './utils/implications' +import { + get_contradiction_string, + get_normalized_functor_implications, + get_proof_string, + type NormalizedImplication, +} from './utils/implications' import type { StructureType } from './config' /** @@ -31,8 +34,8 @@ export function get_deduced_satisfied_properties( stop_when_found?: string }, type: StructureType, - // used for source and target properties of a functor - associated_satisfied_properties?: Record>, + source_props?: Set, + target_props?: Set, ) { const found = new Set() const proofs: Record = {} @@ -49,15 +52,21 @@ export function get_deduced_satisfied_properties( if (!is_valid) continue - if (implication.associated_assumptions) { - const is_applicable = Object.keys( - implication.associated_assumptions, - ).every((key) => { - return is_subset( - implication.associated_assumptions?.[key] ?? new Set(), - associated_satisfied_properties?.[key] ?? new Set(), - ) - }) + if (implication.source_assumptions) { + const is_applicable = is_subset( + implication.source_assumptions, + source_props ?? new Set(), + ) + + if (!is_applicable) continue + } + + if (implication.target_assumptions) { + const is_applicable = is_subset( + implication.target_assumptions, + target_props ?? new Set(), + ) + if (!is_applicable) continue } @@ -101,8 +110,8 @@ export function get_deduced_unsatisfied_properties( stop_when_found?: string }, type: StructureType, - // used for source and target properties of a functor - associated_satisfied_properties?: Record>, + source_props?: Set, + target_props?: Set, ) { const found = new Set() const proofs: Record = {} @@ -122,15 +131,19 @@ export function get_deduced_unsatisfied_properties( }) if (!is_valid) continue - if (implication.associated_assumptions) { - const is_applicable = Object.keys( - implication.associated_assumptions, - ).every((key) => { - return is_subset( - implication.associated_assumptions?.[key] ?? new Set(), - associated_satisfied_properties?.[key] ?? new Set(), - ) - }) + if (implication.source_assumptions) { + const is_applicable = is_subset( + implication.source_assumptions, + source_props ?? new Set(), + ) + if (!is_applicable) continue + } + + if (implication.target_assumptions) { + const is_applicable = is_subset( + implication.target_assumptions, + target_props ?? new Set(), + ) if (!is_applicable) continue } @@ -180,14 +193,14 @@ function save_satisfied_properties( const err_msg = `❌ Failed to complete deduction of satisfied properties for ${structure_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` const property_insert = db.prepare(` - INSERT INTO ${type}_property_assignments - (${type}_id, property_id, is_satisfied, proof, is_deduced) - VALUES (?, ?, TRUE, ?, TRUE) + INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, is_deduced, proof) + VALUES (?, ?, ?, TRUE, TRUE, ?) `) try { for (const p of found) { - property_insert.run(structure_id, p, proofs[p]) + property_insert.run(structure_id, p, type, proofs[p]) } } catch (err) { if (err instanceof SqliteError) { @@ -217,14 +230,14 @@ function save_unsatisfied_properties( const err_msg = `❌ Failed to complete deduction of unsatisfied properties for ${structure_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` const property_insert = db.prepare(` - INSERT INTO ${type}_property_assignments - (${type}_id, property_id, is_satisfied, proof, is_deduced) - VALUES (?, ?, FALSE, ?, TRUE) + INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, is_deduced, proof) + VALUES (?, ?, ?, FALSE, TRUE, ?) `) try { for (const p of found) { - property_insert.run(structure_id, p, proofs[p]) + property_insert.run(structure_id, p, type, proofs[p]) } } catch (err) { if (err instanceof SqliteError) { @@ -257,7 +270,8 @@ function deduce_satisfied_properties( implications, { properties_dict }, type, - structure.associated_satisfied_properties, + structure.source_props, + structure.target_props, ) for (const p of found) satisfied_properties.add(p) @@ -287,7 +301,8 @@ function deduce_unsatisfied_properties( implications, { properties_dict }, type, - structure.associated_satisfied_properties, + structure.source_props, + structure.target_props, ) for (const p of found) unsatisfied_properties.add(p) @@ -342,9 +357,9 @@ function deduce_dual_properties( } const property_insert = db.prepare(` - INSERT INTO ${type}_property_assignments - (${type}_id, property_id, is_satisfied, proof, is_deduced) - VALUES (?, ?, ?, ?, TRUE) + INSERT INTO property_assignments + (structure_id, property_id, type, is_satisfied, is_deduced, proof) + VALUES (?, ?, ?, ?, TRUE, ?) `) const proof_satisfied = `Its dual ${type} satisfies the dual property.` @@ -352,7 +367,7 @@ function deduce_dual_properties( const proof_undecidable = `The dual property is undecidable for its dual ${type}.` for (const p of new_satisfied) { - property_insert.run(structure.id, p, 1, proof_satisfied) + property_insert.run(structure.id, p, type, 1, proof_satisfied) } console.info( @@ -360,7 +375,7 @@ function deduce_dual_properties( ) for (const q of new_unsatisfied) { - property_insert.run(structure.id, q, 0, proof_unsatisfied) + property_insert.run(structure.id, q, type, 0, proof_unsatisfied) } console.info( @@ -368,7 +383,7 @@ function deduce_dual_properties( ) for (const q of new_undecidable) { - property_insert.run(structure.id, q, null, proof_undecidable) + property_insert.run(structure.id, q, type, null, proof_undecidable) } console.info( @@ -380,7 +395,10 @@ function deduce_dual_properties( * Clears all the deduced properties. This runs before the deduction starts. */ function delete_deduced_properties(db: Database, type: StructureType) { - db.prepare(`DELETE FROM ${type}_property_assignments WHERE is_deduced = TRUE`).run() + db.prepare( + `DELETE FROM property_assignments + WHERE is_deduced = TRUE AND type = ?`, + ).run(type) } /** @@ -393,14 +411,15 @@ export function deduce_properties_for_structures(type: StructureType) { const db = get_client() - const implications = get_normalized_implications(db, type) + delete_deduced_properties(db, type) + + const implications = get_normalized_functor_implications(db, type) const structures = get_structures(db, type) + const properties_dict = get_properties_dict(db, type) const get_assigned_properties = get_property_assignments(db, structures, type) const deduction = db.transaction(() => { - delete_deduced_properties(db, type) - for (const structure of structures) { const assigned = get_assigned_properties[structure.id] diff --git a/databases/catdat/scripts/deduce.ts b/databases/catdat/scripts/deduce.ts index f0c72614..0c6a3091 100644 --- a/databases/catdat/scripts/deduce.ts +++ b/databases/catdat/scripts/deduce.ts @@ -1,9 +1,8 @@ -import { deduce_category_implications } from './deduce-category-implications' -import { deduce_functor_implications } from './deduce-functor-implications' import { deduce_special_objects } from './deduce-special-objects' import { deduce_special_morphisms } from './deduce-special-morphisms' import { deduce_properties_for_structures } from './deduce-structure-properties' import { restrict_functor_properties } from './restrict-functor-properties' +import { deduce_implications } from './deduce-implications' deduce() @@ -11,13 +10,12 @@ deduce() * Makes deductions for categories and functors. */ function deduce() { - deduce_category_implications() - deduce_properties_for_structures('category') + deduce_implications() deduce_special_objects() deduce_special_morphisms() + deduce_properties_for_structures('category') restrict_functor_properties() - deduce_functor_implications() deduce_properties_for_structures('functor') } diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index 00c8b649..02a36a8f 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -1,16 +1,19 @@ import { get_client } from './utils/helpers' -import { - get_categories, - get_normalized_category_implications, - type NormalizedCategoryImplication, -} from './utils/categories' +import { get_categories } from './utils/categories' import { get_deduced_satisfied_properties, get_deduced_unsatisfied_properties, } from './deduce-structure-properties' -import { get_property_assignments_by_deduction, StructureMeta } from './utils/deduction' -import { get_functors, get_normalized_functor_implications } from './utils/functors' -import { StructureType } from './config' +import { + get_property_assignments_by_deduction, + type StructureMeta, +} from './utils/deduction' +import { get_functors } from './utils/functors' +import type { StructureType } from './config' +import { + get_normalized_functor_implications, + NormalizedImplication, +} from './utils/implications' const db = get_client() @@ -33,16 +36,12 @@ function check_redundancies() { function check_redundant_property_assignments(type: StructureType) { console.info(`\n--- Check redundant ${type} property assignments ---`) - // TODO: refactor this when > 2 types of structures are available - const implications = - type === 'category' - ? get_normalized_category_implications(db) - : get_normalized_functor_implications(db) + const implications = get_normalized_functor_implications(db, type) const structures: StructureMeta[] = type === 'category' ? get_categories(db) : get_functors(db) - const assignments = get_property_assignments_by_deduction(db, structures, type) + const assignments = get_property_assignments_by_deduction(db, type) const ignore_dict = get_ignored_redundant_assignments(type) const ignore_count = Object.keys(ignore_dict).reduce( @@ -57,7 +56,8 @@ function check_redundant_property_assignments(type: StructureType) { assignments[structure.id].satisfied.non_deduced, implications, ignore_dict[structure.id], - structure.associated_satisfied_properties, + structure.source_props, + structure.target_props, ) if (redundant_satisfied_property) { @@ -78,7 +78,8 @@ function check_redundant_property_assignments(type: StructureType) { assignments[structure.id].unsatisfied.non_deduced, implications, ignore_dict[structure.id], - structure.associated_satisfied_properties, + structure.source_props, + structure.target_props, ) if (redundant_unsatisfied_property) { @@ -109,9 +110,10 @@ function check_redundant_property_assignments(type: StructureType) { */ function get_redundant_satisfied_property( satisfied_properties: Set, - implications: NormalizedCategoryImplication[], + implications: NormalizedImplication[], ignored: Set = new Set(), - associated_satisfied_properties?: Record>, + source_props?: Set, + target_props?: Set, ) { for (const p of [...satisfied_properties]) { if (ignored.has(p)) continue @@ -121,7 +123,8 @@ function get_redundant_satisfied_property( implications, { stop_when_found: p }, 'category', - associated_satisfied_properties, + source_props, + target_props, ) if (deduced_satisfied_properties.has(p)) return p satisfied_properties.add(p) @@ -138,9 +141,10 @@ function get_redundant_satisfied_property( function get_redundant_unsatisfied_property( satisfied_properties: Set, unsatisfied_properties: Set, - implications: NormalizedCategoryImplication[], + implications: NormalizedImplication[], ignored: Set = new Set(), - associated_satisfied_properties?: Record>, + source_props?: Set, + target_props?: Set, ) { for (const p of [...unsatisfied_properties]) { if (ignored.has(p)) continue @@ -151,7 +155,8 @@ function get_redundant_unsatisfied_property( implications, { stop_when_found: p }, 'category', - associated_satisfied_properties, + source_props, + target_props, ) if (deduced_unsatisfied_properties.has(p)) return p unsatisfied_properties.add(p) @@ -166,12 +171,12 @@ function get_redundant_unsatisfied_property( */ function get_ignored_redundant_assignments(type: StructureType) { const rows = db - .prepare( - `SELECT ${type}_id as structure_id, property_id - FROM ${type}_property_assignments - WHERE check_redundancy = FALSE`, + .prepare<[string], { structure_id: string; property_id: string }>( + `SELECT structure_id, property_id + FROM property_assignments + WHERE type = ? AND check_redundancy = FALSE`, ) - .all() as { structure_id: string; property_id: string }[] + .all(type) const grouped: Record> = {} diff --git a/databases/catdat/scripts/restrict-functor-properties.ts b/databases/catdat/scripts/restrict-functor-properties.ts index c3c06732..5e9aa39e 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -4,38 +4,40 @@ const db = get_client() /** * Ensures that selected properties of functors are restricted - * to specified source and target categories. + * to specified target categories. + * This can be extended to source categories if required. */ export function restrict_functor_properties() { console.info('\n--- Restrict functor properties ---') - for (const domain of ['source', 'target']) { - const res = db - .prepare( - `INSERT INTO functor_property_assignments ( - functor_id, - property_id, - is_satisfied, - proof, - is_deduced, - check_redundancy - ) - SELECT - f.id, - p.id, - FALSE, - 'The ${domain} category is not ' || c.notation || '.', - FALSE, - FALSE - FROM functor_properties p - INNER JOIN categories c ON c.id = p.required_${domain} - JOIN functors f - WHERE f.${domain} <> p.required_${domain}`, - ) - .run() - - console.info( - `Restricted ${res.changes} functor properties based on their required ${domain}`, + const res = db + .prepare( + `INSERT INTO property_assignments ( + type, + structure_id, + property_id, + is_satisfied, + proof, + is_deduced, + check_redundancy + ) + SELECT + 'functor', + f.id, + r.functor_property_id, + FALSE, + 'The target category is not ' || c.notation || '.', + FALSE, + FALSE + FROM required_target_categories r + INNER JOIN categories_view c ON c.id = r.category_id + JOIN functors f + WHERE f.target <> r.category_id + ON CONFLICT DO NOTHING`, ) - } + .run() + + console.info( + `Restricted ${res.changes} functor properties based on their required target`, + ) } diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index c38f5b81..dde93f80 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -1,18 +1,17 @@ import path from 'node:path' -import { get_client, seed_file, seed_files } from './utils/helpers' +import { get_client, seed_file, seed_files, pluralize } from './utils/helpers' +import { create_schema_hash, get_saved_schema_hash } from './utils/schema' +import { PROOF_LENGTH_THRESHOLD, STRUCTURE_MAPS, type StructureType } from './config' import type { CategoryYaml, ConfigYaml, - CategoryPropertyYaml, - CategoryImplicationYaml, - FunctorImplicationYaml, - FunctorPropertyYaml, + PropertyYaml, FunctorYaml, ProofWarning, PropertyEntry, + StructureYaml, + ImplicationYaml, } from './seed.types' -import { create_schema_hash, get_saved_schema_hash } from './utils/schema' -import { PLURALS, PROOF_LENGTH_THRESHOLD, STRUCTURES } from './config' const db = get_client() @@ -40,13 +39,13 @@ function seed() { seed_config() - seed_category_properties() - seed_category_implications() - seed_categories() + seed_properties('category') + seed_implications('category') + seed_structures('category', insert_category) - seed_functor_properties() - seed_functor_implications() - seed_functors() + seed_properties('functor') + seed_implications('functor') + seed_structures('functor') print_proof_length_warnings() } @@ -58,33 +57,32 @@ function clear_all_tables() { console.info(`\nClear all tables ...`) const tx = db.transaction(() => { - db.pragma('foreign_keys = OFF') - db.prepare(`DELETE FROM special_morphisms`).run() db.prepare(`DELETE FROM special_morphism_types`).run() db.prepare(`DELETE FROM special_objects`).run() db.prepare(`DELETE FROM special_object_types`).run() - db.prepare(`DELETE FROM functor_implication_source_assumptions`).run() - db.prepare(`DELETE FROM functor_implication_target_assumptions`).run() - db.prepare(`DELETE FROM adjoint_functors`).run() - - for (const type of STRUCTURES) { - const plural = PLURALS[type] - - db.prepare(`DELETE FROM ${type}_implication_assumptions`).run() - db.prepare(`DELETE FROM ${type}_implication_conclusions`).run() - db.prepare(`DELETE FROM ${type}_implications`).run() - db.prepare(`DELETE FROM ${type}_property_assignments`).run() - db.prepare(`DELETE FROM ${type}_comments`).run() - db.prepare(`DELETE FROM related_${plural}`).run() - db.prepare(`DELETE FROM ${type}_tag_assignments`).run() - db.prepare(`DELETE FROM related_${type}_properties`).run() - db.prepare(`DELETE FROM ${type}_properties`).run() - db.prepare(`DELETE FROM ${plural}`).run() - db.prepare(`DELETE FROM ${type}_tags`).run() - } + db.prepare(`DELETE FROM structure_map_values`).run() + + db.prepare(`DELETE FROM assumptions`).run() + db.prepare(`DELETE FROM mapped_assumptions`).run() + db.prepare(`DELETE FROM conclusions`).run() + db.prepare(`DELETE FROM implications`).run() + db.prepare(`DELETE FROM property_assignments`).run() + db.prepare(`DELETE FROM related_properties`).run() + db.prepare(`DELETE FROM dual_properties`).run() + db.prepare(`DELETE FROM properties`).run() + + db.prepare(`DELETE FROM related_structures`).run() + db.prepare(`DELETE FROM dual_structures`).run() + db.prepare(`DELETE FROM structure_comments`).run() + db.prepare(`DELETE FROM tag_assignments`).run() + db.prepare(`DELETE FROM structures`).run() + + db.prepare(`DELETE FROM categories`).run() + + db.prepare(`DELETE FROM tags`).run() db.prepare(`DELETE FROM relations`).run() }) @@ -100,8 +98,7 @@ function clear_all_tables() { * Seeds the data from the global config file `config.yaml`. */ function seed_config() { - const category_tag_insert = db.prepare(`INSERT INTO category_tags (tag) VALUES (?)`) - const functor_tag_insert = db.prepare(`INSERT INTO functor_tags (tag) VALUES (?)`) + const tag_insert = db.prepare(`INSERT INTO tags (tag, type) VALUES (?, ?)`) const relation_insert = db.prepare( `INSERT INTO relations (relation, conditional) VALUES (?, ?)`, @@ -117,16 +114,16 @@ function seed_config() { function insert_config(config: ConfigYaml) { for (const tag of config.shared_tags) { - category_tag_insert.run(tag) - functor_tag_insert.run(tag) + tag_insert.run(tag, 'category') + tag_insert.run(tag, 'functor') } for (const tag of config.category_tags) { - category_tag_insert.run(tag) + tag_insert.run(tag, 'category') } for (const tag of config.functor_tags) { - functor_tag_insert.run(tag) + tag_insert.run(tag, 'functor') } for (const { relation, conditional } of config.relations) { @@ -146,135 +143,98 @@ function seed_config() { } /** - * Seeds all properties of categories from YAML files. + * Seeds all properties of a given structure type from YAML files. */ -function seed_category_properties() { +function seed_properties(type: StructureType) { const property_insert = db.prepare( - `INSERT INTO category_properties ( - id, relation, description, nlab_link, - dual_property_id, invariant_under_equivalences + `INSERT INTO properties ( + id, type, relation, description, nlab_link, + invariant_under_equivalences ) VALUES (?, ?, ?, ?, ?, ?)`, ) const related_insert = db.prepare( - `INSERT INTO related_category_properties - (property_id, related_property_id) - VALUES (?, ?)`, + `INSERT INTO related_properties (property, related_property, type) VALUES (?, ?, ?)`, ) - function insert_property(property: CategoryPropertyYaml) { + const dual_insert = db.prepare( + `INSERT INTO dual_properties (property, dual_property, type) VALUES (?, ?, ?)`, + ) + + function insert_property(property: PropertyYaml) { property_insert.run( property.id, + type, property.relation, property.description, property.nlab_link || null, - property.dual_property || null, Number(property.invariant_under_equivalences), ) for (const related of property.related_properties) { - related_insert.run(property.id, related) + related_insert.run(property.id, related, type) } - } - - seed_files( - db, - 'category properties', - path.join(data_folder, 'category-properties'), - insert_property, - ) -} -/** - * Seeds all implications between category properties from YAML files. - */ -function seed_category_implications() { - const implication_insert = db.prepare( - `INSERT INTO category_implications ( - id, proof, is_equivalence - ) VALUES (?, ?, ?)`, - ) - - const assumption_insert = db.prepare( - `INSERT INTO category_implication_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) - - const conclusion_insert = db.prepare( - `INSERT INTO category_implication_conclusions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) - - function insert_implications(implications: CategoryImplicationYaml[]) { - for (const impl of implications) { - implication_insert.run(impl.id, impl.proof, Number(impl.is_equivalence)) - - for (const assumption of impl.assumptions) { - assumption_insert.run(impl.id, assumption) - } - - for (const conclusion of impl.conclusions) { - conclusion_insert.run(impl.id, conclusion) - } + if (property.dual_property) { + dual_insert.run(property.id, property.dual_property, type) } } seed_files( db, - 'category implications', - path.join(data_folder, 'category-implications'), - insert_implications, + `${type} properties`, + path.join(data_folder, `${type}-properties`), + insert_property, ) } /** - * Seeds all categories from YAML files, including their property assignments. + * Seeds all structures of a given type from YAML files, + * including their related structures and property assignments. */ -function seed_categories() { - const category_insert = db.prepare( - `INSERT INTO categories ( - id, name, notation, objects, morphisms, - description, nlab_link, dual_category_id - ) VALUES (?, ?, ?, ?, ?, ?, ?, ?)`, +function seed_structures< + Struct extends StructureYaml & { source?: string; target?: string }, +>(type: StructureType, extra?: (item: Struct) => void) { + const structure_insert = db.prepare( + `INSERT INTO structures ( + id, type, name, notation, description, nlab_link + ) VALUES (?, ?, ?, ?, ?, ?)`, + ) + + const value_insert = db.prepare( + `INSERT INTO structure_map_values + (map, input, input_type, output, output_type) + VALUES (?, ?, ?, ?, ?)`, ) const tag_insert = db.prepare( - `INSERT INTO category_tag_assignments (category_id, tag) VALUES (?, ?)`, + `INSERT INTO tag_assignments (structure, type, tag) VALUES (?, ?, ?)`, ) const comment_insert = db.prepare( - `INSERT INTO category_comments (category_id, comment) VALUES (?, ?)`, + `INSERT INTO structure_comments (structure, type, comment) VALUES (?, ?, ?)`, ) const related_insert = db.prepare( - `INSERT INTO related_categories (category_id, related_category_id) VALUES (?, ?)`, - ) - - const special_object_insert = db.prepare( - `INSERT INTO special_objects (category_id, type, description) VALUES (?, ?, ?)`, - ) - - const special_morphism_insert = db.prepare( - `INSERT INTO special_morphisms (category_id, type, description, proof) - VALUES (?, ?, ?, ?)`, + `INSERT INTO related_structures (structure, related_structure, type) VALUES (?, ?, ?)`, ) const property_assignment_insert = db.prepare( - `INSERT INTO category_property_assignments ( - category_id, property_id, is_satisfied, proof, check_redundancy - ) VALUES (?, ?, ?, ?, ?)`, + `INSERT INTO property_assignments ( + type, structure, property, + is_satisfied, proof, check_redundancy + ) VALUES (?, ?, ?, ?, ?, ?)`, ) function insert_property_assignments( - category_id: string, + structure_id: string, entries: PropertyEntry[], is_satisfied: 0 | 1 | null, ) { for (const entry of entries) { property_assignment_insert.run( - category_id, + type, + structure_id, entry.property, is_satisfied, entry.proof, @@ -282,7 +242,8 @@ function seed_categories() { ) if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { proof_length_warnings.push({ - structure_id: category_id, + structure: structure_id, + type, property: entry.property, length: entry.proof.length, }) @@ -290,253 +251,149 @@ function seed_categories() { } } - function insert_category(category: CategoryYaml) { - category_insert.run( - category.id, - category.name, - category.notation, - category.objects, - category.morphisms, - category.description, - category.nlab_link, - category.dual_category || null, + function insert_structure(structure: Struct) { + structure_insert.run( + structure.id, + type, + structure.name, + structure.notation, + structure.description, + structure.nlab_link, ) - for (const tag of category.tags) { - tag_insert.run(category.id, tag) - } - - for (const comment of category.comments ?? []) { - comment_insert.run(category.id, comment) + for (const map in STRUCTURE_MAPS[type]) { + const val = structure[map] + if (!val) continue + const val_type = STRUCTURE_MAPS[type][map] + value_insert.run(map, structure.id, type, val, val_type) } - for (const related of category.related_categories) { - related_insert.run(category.id, related) + for (const tag of structure.tags) { + tag_insert.run(structure.id, type, tag) } - for (const [type, entry] of Object.entries(category.special_objects)) { - if (!entry) continue - special_object_insert.run(category.id, type, entry.description) + for (const comment of structure.comments ?? []) { + comment_insert.run(structure.id, type, comment) } - for (const [type, entry] of Object.entries(category.special_morphisms)) { - if (!entry) continue - special_morphism_insert.run(category.id, type, entry.description, entry.proof) + for (const related of structure.related) { + related_insert.run(structure.id, related, type) } - insert_property_assignments(category.id, category.satisfied_properties, 1) - insert_property_assignments(category.id, category.unsatisfied_properties, 0) + insert_property_assignments(structure.id, structure.satisfied_properties, 1) + insert_property_assignments(structure.id, structure.unsatisfied_properties, 0) insert_property_assignments( - category.id, - category.undecidable_properties ?? [], + structure.id, + structure.undecidable_properties ?? [], null, ) - } - - seed_files(db, 'categories', path.join(data_folder, 'categories'), insert_category) -} - -/** - * Seeds all properties of functors from YAML files. - */ -function seed_functor_properties() { - const property_insert = db.prepare(` - INSERT INTO functor_properties ( - id, relation, description, - required_source, required_target, - nlab_link, dual_property_id, - invariant_under_equivalences - ) VALUES (?, ?, ?, ?, ?, ?, ?, ?)`) - - const related_insert = db.prepare( - `INSERT INTO related_functor_properties - (property_id, related_property_id) - VALUES (?, ?)`, - ) - - function insert_property(property: FunctorPropertyYaml) { - property_insert.run( - property.id, - property.relation, - property.description, - property.required_source || null, - property.required_target || null, - property.nlab_link || null, - property.dual_property || null, - Number(property.invariant_under_equivalences), - ) - for (const related of property.related_properties) { - related_insert.run(property.id, related) - } + if (extra) extra(structure) } seed_files( db, - 'functor properties', - path.join(data_folder, 'functor-properties'), - insert_property, + pluralize(type), + path.join(data_folder, pluralize(type)), + insert_structure, ) } /** - * Seeds all implications between functor properties from YAML files. + * Inserts the data of a category that is only relevant for categories. */ -function seed_functor_implications() { - const implication_insert = db.prepare( - `INSERT INTO functor_implications ( - id, proof, is_equivalence - ) VALUES (?, ?, ?)`, - ) +function insert_category(category: CategoryYaml) { + const category_insert = db.prepare(` + INSERT INTO categories (id, objects, morphisms) VALUES (?, ?, ?) + `) - const assumption_insert = db.prepare( - `INSERT INTO functor_implication_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) + const dual_insert = db.prepare(` + INSERT INTO dual_structures (type, structure, dual_structure) + VALUES ('category', ?, ?)`) - const source_assumption_insert = db.prepare( - `INSERT INTO functor_implication_source_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, - ) - - const target_assumption_insert = db.prepare( - `INSERT INTO functor_implication_target_assumptions ( - implication_id, property_id - ) VALUES (?, ?)`, + const special_object_insert = db.prepare( + `INSERT INTO special_objects (category, type, description) VALUES (?, ?, ?)`, ) - const conclusion_insert = db.prepare( - `INSERT INTO functor_implication_conclusions ( - implication_id, property_id - ) VALUES (?, ?)`, + const special_morphism_insert = db.prepare( + `INSERT INTO special_morphisms (category, type, description, proof) + VALUES (?, ?, ?, ?)`, ) - function insert_implications(implications: FunctorImplicationYaml[]) { - for (const impl of implications) { - implication_insert.run(impl.id, impl.proof, Number(impl.is_equivalence)) - - for (const assumption of impl.assumptions) { - assumption_insert.run(impl.id, assumption) - } - - for (const assumption of impl.source_assumptions) { - source_assumption_insert.run(impl.id, assumption) - } + category_insert.run(category.id, category.objects, category.morphisms) - for (const assumption of impl.target_assumptions) { - target_assumption_insert.run(impl.id, assumption) - } + if (category.dual_category) { + dual_insert.run(category.id, category.dual_category) + } - for (const conclusion of impl.conclusions) { - conclusion_insert.run(impl.id, conclusion) - } - } + for (const [type, entry] of Object.entries(category.special_objects)) { + if (!entry) continue + special_object_insert.run(category.id, type, entry.description) } - seed_files( - db, - 'functor implications', - path.join(data_folder, 'functor-implications'), - insert_implications, - ) + for (const [type, entry] of Object.entries(category.special_morphisms)) { + if (!entry) continue + special_morphism_insert.run(category.id, type, entry.description, entry.proof) + } } /** - * Seeds all functors from YAML files. + * Seeds all implications between properties from YAML files. */ -function seed_functors() { - const functor_insert = db.prepare( - `INSERT INTO functors ( - id, name, notation, source, target, description, nlab_link - ) VALUES (?, ?, ?, ?, ?, ?, ?)`, - ) - - const tag_insert = db.prepare( - `INSERT INTO functor_tag_assignments (functor_id, tag) VALUES (?, ?)`, - ) - - const comment_insert = db.prepare( - `INSERT INTO functor_comments (functor_id, comment) VALUES (?, ?)`, +function seed_implications(type: StructureType) { + const implication_insert = db.prepare( + `INSERT INTO implications ( + id, type, proof, is_equivalence + ) VALUES (?, ?, ?, ?)`, ) - const related_insert = db.prepare( - `INSERT INTO related_functors (functor_id, related_functor_id) VALUES (?, ?)`, + const assumption_insert = db.prepare( + `INSERT INTO assumptions (implication, property, type) VALUES (?, ?, ?)`, ) - const adjoint_insert = db.prepare( - `INSERT INTO adjoint_functors (left_adjoint, right_adjoint) - VALUES (?, ?) - ON CONFLICT (left_adjoint, right_adjoint) DO NOTHING`, + const mapped_assumption_insert = db.prepare( + `INSERT INTO mapped_assumptions + (map, implication, implication_type, property, property_type) + VALUES (?, ?, ?, ?, ?)`, ) - const property_assignment_insert = db.prepare( - `INSERT INTO functor_property_assignments ( - functor_id, property_id, is_satisfied, proof, check_redundancy - ) VALUES (?, ?, ?, ?, ?)`, + const conclusion_insert = db.prepare( + `INSERT INTO conclusions (implication, property, type) VALUES (?, ?, ?)`, ) - function insert_property_assignments( - functor_id: string, - entries: PropertyEntry[], - is_satisfied: 0 | 1 | null, - ) { - for (const entry of entries) { - property_assignment_insert.run( - functor_id, - entry.property, - is_satisfied, - entry.proof, - entry.check_redundancy === false ? 0 : 1, - ) - if (entry.proof.length >= PROOF_LENGTH_THRESHOLD) { - proof_length_warnings.push({ - structure_id: functor_id, - property: entry.property, - length: entry.proof.length, - }) - } - } - } - - function insert_functor(functor: FunctorYaml) { - functor_insert.run( - functor.id, - functor.name, - functor.notation, - functor.source, - functor.target, - functor.description || null, - functor.nlab_link || null, - ) + function insert_implication(impl: ImplicationYaml) { + implication_insert.run(impl.id, type, impl.proof, Number(impl.is_equivalence)) - for (const tag of functor.tags) { - tag_insert.run(functor.id, tag) + for (const p of impl.assumptions) { + assumption_insert.run(impl.id, p, type) } - if (functor.left_adjoint) { - adjoint_insert.run(functor.left_adjoint, functor.id) + for (const q of impl.conclusions) { + conclusion_insert.run(impl.id, q, type) } - for (const comment of functor.comments ?? []) { - comment_insert.run(functor.id, comment) + if (impl.mapped_assumptions) { + for (const map in impl.mapped_assumptions) { + const prop_type = STRUCTURE_MAPS[type][map] + for (const prop of impl.mapped_assumptions[map]) { + mapped_assumption_insert.run(map, impl.id, type, prop, prop_type) + } + } } + } - for (const related of functor.related_functors) { - related_insert.run(functor.id, related) + function insert_implications(implications: ImplicationYaml[]) { + for (const impl of implications) { + insert_implication(impl) } - - insert_property_assignments(functor.id, functor.satisfied_properties, 1) - insert_property_assignments(functor.id, functor.unsatisfied_properties, 0) - insert_property_assignments( - functor.id, - functor.undecidable_properties ?? [], - null, - ) } - seed_files(db, 'functors', path.join(data_folder, 'functors'), insert_functor) + seed_files( + db, + `${type} implications`, + path.join(data_folder, `${type}-implications`), + insert_implications, + ) } function print_proof_length_warnings() { @@ -546,9 +403,9 @@ function print_proof_length_warnings() { proof_length_warnings.sort((a, b) => b.length - a.length) - for (const { structure_id, property, length } of proof_length_warnings) { + for (const { structure, type, property, length } of proof_length_warnings) { console.warn( - `🟡 The proof for (${structure_id}, ${property}) has ${length} characters. Consider moving it to a content page.`, + `🟡 The proof for (${structure}, ${property}) of type ${type} has ${length} characters. Consider moving it to a content page.`, ) } } diff --git a/databases/catdat/scripts/seed.types.ts b/databases/catdat/scripts/seed.types.ts index a08e1c66..1c1012bd 100644 --- a/databases/catdat/scripts/seed.types.ts +++ b/databases/catdat/scripts/seed.types.ts @@ -1,114 +1,71 @@ +import { StructureType } from './config' + export type ConfigYaml = { shared_tags: string[] category_tags: string[] functor_tags: string[] - relations: { - relation: string - conditional: string - }[] - special_object_types: { - type: string - dual: string - }[] - special_morphism_types: { - type: string - dual: string - }[] + relations: { relation: string; conditional: string }[] + special_object_types: { type: string; dual: string }[] + special_morphism_types: { type: string; dual: string }[] +} + +export type PropertyEntry = { + property: string + proof: string + check_redundancy?: boolean } -export type CategoryYaml = { +export type StructureYaml = { id: string name: string notation: string - objects: string - morphisms: string description: string | null nlab_link: string | null - dual_category?: string | null tags: string[] - related_categories: string[] + comments?: string[] + related: string[] satisfied_properties: PropertyEntry[] unsatisfied_properties: PropertyEntry[] undecidable_properties?: PropertyEntry[] - special_objects: Record - special_morphisms: Record - comments?: string[] } -export type PropertyEntry = { - property: string - proof: string - check_redundancy?: boolean -} - -type ObjectEntry = { - description: string +export type CategoryYaml = StructureYaml & { + objects: string + morphisms: string + dual_category?: string + special_objects: Record + special_morphisms: Record } -type MorphismEntry = { - description: string - proof: string +export type FunctorYaml = StructureYaml & { + source: string + target: string + left_adjoint?: string } -export type CategoryPropertyYaml = { +export type PropertyYaml = { id: string relation: string description: string nlab_link?: string | null dual_property?: string | null + required_target?: string // for functors, TODO: bring back this feature invariant_under_equivalences: boolean related_properties: string[] } -export type CategoryImplicationYaml = { - id: string - assumptions: string[] - conclusions: string[] - proof: string - is_equivalence: boolean -} - -export type FunctorImplicationYaml = { +export type ImplicationYaml = { id: string assumptions: string[] - source_assumptions: string[] - target_assumptions: string[] conclusions: string[] + mapped_assumptions?: Record proof: string is_equivalence: boolean } -export type FunctorPropertyYaml = { - id: string - relation: string - description: string - required_source?: string - required_target?: string - nlab_link?: string | null - dual_property?: string | null - invariant_under_equivalences: boolean - related_properties: string[] -} - -export type FunctorYaml = { - id: string - name: string - notation: string - source: string - target: string - description?: string | null - nlab_link?: string - left_adjoint?: string - tags: string[] - related_functors: string[] - satisfied_properties: PropertyEntry[] - unsatisfied_properties: PropertyEntry[] - undecidable_properties?: PropertyEntry[] - comments?: string[] -} - export type ProofWarning = { - structure_id: string + structure: string + type: string property: string length: number } diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index ca019581..a9d31a7b 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -24,22 +24,23 @@ execute_tests() function execute_tests() { try { console.info('\n--- Test categories ---') - test_mutual_category_duals() + test_mutual_structure_duals('category') test_properties_of_trivial_category() test_mutual_property_duals('category') test_decided_structures(decided_categories, 'category') - test_properties_of_selected_structures( - { Set: Set_expected, Ab: Ab_expected, Top: Top_expected }, - 'category', - ) + test_properties_of_selected_structures({ + Set: Set_expected, + Ab: Ab_expected, + Top: Top_expected, + }) console.info('\n--- Test functors ---') test_mutual_property_duals('functor') test_decided_structures(decided_functors, 'functor') - test_properties_of_selected_structures( - { forget_vector: forget_vector_expected, id_Set: id_Set_expected }, - 'functor', - ) + test_properties_of_selected_structures({ + forget_vector: forget_vector_expected, + id_Set: id_Set_expected, + }) } catch (err) { if (err instanceof Error) { console.error(err.message) @@ -51,27 +52,30 @@ function execute_tests() { } /** - * Tests for all categories C,D that if C is dual to D, then D is dual to C. + * Tests for all structures C,D that if C is dual to D, then D is dual to C. */ -function test_mutual_category_duals() { +function test_mutual_structure_duals(type: StructureType) { const dict: Record = {} - const categories = db - .prepare('SELECT id, dual_category_id FROM categories') - .all() as { id: string; dual_category_id: string | null }[] + const structures = db + .prepare<[string], { id: string; dual_structure_id: string | null }>( + `SELECT structure_id as id, dual_structure_id + FROM dual_structures WHERE type = ?`, + ) + .all(type) - for (const { id, dual_category_id } of categories) { - dict[id] = dual_category_id + for (const { id, dual_structure_id } of structures) { + dict[id] = dual_structure_id } for (const id in dict) { const dual = dict[id] if (dual && dict[dual] !== id) { - throw new Error(`❌ Found non-mutual category duality: ${id}, ${dual}`) + throw new Error(`❌ Found non-mutual structure duality: ${id}, ${dual}`) } } - console.info(`✅ Categories are mutually dual`) + console.info(`✅ Structures of type ${type} are mutually dual`) } /** @@ -81,8 +85,10 @@ function test_mutual_category_duals() { function test_properties_of_trivial_category() { const rows = db .prepare( - `SELECT property_id FROM category_property_assignments - WHERE category_id = '1' AND is_satisfied = FALSE`, + `SELECT property_id FROM property_assignments + WHERE + type = 'category' AND structure_id = '1' + AND is_satisfied = FALSE`, ) .all() @@ -100,11 +106,14 @@ function test_properties_of_trivial_category() { * if p is dual to q, then q is dual to p. */ function test_mutual_property_duals(type: StructureType) { - const dict: Record = {} + const dict: Record = {} const properties = db - .prepare(`SELECT id, dual_property_id FROM ${type}_properties`) - .all() as { id: string; dual_property_id: string | null }[] + .prepare<[string], { id: string; dual_property_id: string }>( + `SELECT property_id AS id, dual_property_id + FROM dual_properties WHERE type = ?`, + ) + .all(type) for (const { id, dual_property_id } of properties) { dict[id] = dual_property_id @@ -112,7 +121,7 @@ function test_mutual_property_duals(type: StructureType) { for (const id in dict) { const dual = dict[id] - if (dual && dict[dual] !== id) { + if (dict[dual] !== id) { throw new Error(`❌ Found non-mutual property duality: ${id}, ${dual}`) } } @@ -125,17 +134,18 @@ function test_mutual_property_duals(type: StructureType) { * been decided. If this test fails, property assignments or implications are missing. */ function test_decided_structures(structure_ids: string[], type: StructureType) { - const unknown_query = db.prepare( - `SELECT p.id FROM ${type}_properties p WHERE NOT EXISTS - (SELECT 1 FROM ${type}_property_assignments - WHERE ${type}_id = ? AND property_id = p.id + const unknown_query = db.prepare<[string, string], { id: string }>( + `SELECT p.id FROM properties p WHERE type = ? AND NOT EXISTS + (SELECT 1 FROM property_assignments + WHERE structure_id = ? AND property_id = p.id ) `, ) for (const structure_id of structure_ids) { - const res = unknown_query.all(structure_id) as { id: string }[] - const unknown_properties = res.map((row) => row.id) + const unknown_properties = unknown_query + .all(type, structure_id) + .map((row) => row.id) if (unknown_properties.length > 0) { throw new Error( @@ -155,18 +165,17 @@ function test_decided_structures(structure_ids: string[], type: StructureType) { */ function test_properties_of_selected_structures( expected: Record>, - type: StructureType, ) { - const property_query = db.prepare( - `SELECT property_id, is_satisfied FROM ${type}_property_assignments - WHERE ${type}_id = ? AND is_satisfied IS NOT NULL`, + const property_query = db.prepare< + [string], + { property_id: string; is_satisfied: 0 | 1 } + >( + `SELECT property_id, is_satisfied FROM property_assignments + WHERE structure_id = ? AND is_satisfied IS NOT NULL`, ) for (const structure_id in expected) { - const properties = property_query.all(structure_id) as { - property_id: string - is_satisfied: 0 | 1 - }[] + const properties = property_query.all(structure_id) for (const { property_id, is_satisfied } of properties) { const ok = Boolean(is_satisfied) === expected[structure_id][property_id] diff --git a/databases/catdat/scripts/utils/categories.ts b/databases/catdat/scripts/utils/categories.ts index 6c4cb05e..beba613f 100644 --- a/databases/catdat/scripts/utils/categories.ts +++ b/databases/catdat/scripts/utils/categories.ts @@ -1,74 +1,14 @@ import { type Database } from 'better-sqlite3' -import { parse_json_set } from './helpers' - -type CategoryMeta = { - id: string - name: string - dual: string | null -} - -export type NormalizedCategoryImplication = { - id: string - assumptions: Set - conclusion: string -} +import type { StructureMeta } from './deduction' /** * Returns the list of categories saved in the database. */ -export function get_categories(db: Database) { +export function get_categories(db: Database): StructureMeta[] { return db - .prepare( + .prepare( `SELECT id, name, dual_category_id as dual - FROM categories ORDER BY lower(name)`, - ) - .all() as CategoryMeta[] -} - -/** - * Implications have the form - * P_1 + ... + P_n ===> Q_1 + ... + Q_m - * or - * P_1 + ... + P_n <===> Q_1 + ... + Q_m. - * This function decomposes them into normalized implications, - * which have the form - * P_1 + ... + P_n ===> Q. - */ -export function get_normalized_category_implications( - db: Database, -): NormalizedCategoryImplication[] { - const all_implications_db = db - .prepare( - `SELECT id, assumptions, conclusions, is_equivalence - FROM category_implications_view`, + FROM categories_view ORDER BY lower(name)`, ) - .all() as { - id: string - assumptions: string - conclusions: string - is_equivalence: 0 | 1 - }[] - - const implications: NormalizedCategoryImplication[] = [] - - for (const impl of all_implications_db) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - - for (const conclusion of conclusions) { - implications.push({ id: impl.id, assumptions, conclusion }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption, - }) - } - } - } - - return implications + .all() } diff --git a/databases/catdat/scripts/utils/deduction.ts b/databases/catdat/scripts/utils/deduction.ts index 66e654fd..fb2d32f8 100644 --- a/databases/catdat/scripts/utils/deduction.ts +++ b/databases/catdat/scripts/utils/deduction.ts @@ -1,6 +1,6 @@ import { type Database } from 'better-sqlite3' -import { get_categories, get_normalized_category_implications } from './categories' -import { get_functors, get_normalized_functor_implications } from './functors' +import { get_categories } from './categories' +import { get_functors } from './functors' import { StructureType } from '../config' /** @@ -10,16 +10,8 @@ export type StructureMeta = { id: string name: string dual?: string | null - // used for source and target properties of a functor - associated_satisfied_properties?: Record> -} - -export type NormalizedImplication = { - id: string - assumptions: Set - conclusion: string - // used for source and target assumptions of a functor in an implication - associated_assumptions?: Record> + source_props?: Set + target_props?: Set } export type PropertyMeta = { @@ -38,32 +30,22 @@ export function get_structures(db: Database, type: StructureType): StructureMeta throw new Error('Unsupported type') } -/** - * Returns the list of normalized implications saved in the database of a given type. - */ -export function get_normalized_implications( - db: Database, - type: StructureType, -): NormalizedImplication[] { - if (type === 'category') return get_normalized_category_implications(db) - if (type === 'functor') return get_normalized_functor_implications(db) - throw new Error('Unsupported type') -} - /** * Returns a dictionary of properties saved in the database. */ export function get_properties_dict(db: Database, type: StructureType) { const properties = db - .prepare( + .prepare<[string], PropertyMeta>( `SELECT - p.id, p.dual_property_id as dual, p.relation, - r.conditional - FROM ${type}_properties p + p.id, d.dual_property_id as dual, + p.relation, r.conditional + FROM properties p + LEFT JOIN dual_properties d ON d.property_id = p.id INNER JOIN relations r ON r.relation = p.relation + WHERE p.type = ? ORDER BY lower(p.id)`, ) - .all() as PropertyMeta[] + .all(type) const dict: Record = {} @@ -83,19 +65,30 @@ export function get_property_assignments( type: StructureType, ) { const rows = db - .prepare( - `SELECT property_id, ${type}_id as structure_id, is_satisfied - FROM ${type}_property_assignments`, + .prepare< + [string], + { + property_id: string + structure_id: string + is_satisfied: 0 | 1 | null + } + >( + `SELECT + property_id, + structure_id, + is_satisfied + FROM property_assignments + WHERE type = ?`, ) - .all() as { - property_id: string - structure_id: string - is_satisfied: 0 | 1 | null - }[] + .all(type) const grouped: Record< string, - { satisfied: Set; unsatisfied: Set; undecidable: Set } + { + satisfied: Set + unsatisfied: Set + undecidable: Set + } > = {} for (const structure of structures) { @@ -127,22 +120,26 @@ export function get_property_assignments( * grouped by structure, value (satisfied / unsatisfied), and deduced status. * We exclude undecidable properties here. */ -export function get_property_assignments_by_deduction( - db: Database, - structures: { id: string }[], - type: StructureType, -) { +export function get_property_assignments_by_deduction(db: Database, type: StructureType) { const rows = db - .prepare( - `SELECT property_id, ${type}_id as structure_id, is_satisfied, is_deduced - FROM ${type}_property_assignments WHERE is_satisfied IS NOT NULL`, + .prepare< + [string], + { + property_id: string + structure_id: string + is_satisfied: 0 | 1 + is_deduced: 0 | 1 + } + >( + `SELECT + property_id, + structure_id, + is_satisfied, + is_deduced + FROM property_assignments + WHERE is_satisfied IS NOT NULL AND type = ?`, ) - .all() as { - property_id: string - structure_id: string - is_satisfied: 0 | 1 - is_deduced: 0 | 1 - }[] + .all(type) const grouped: Record< string, @@ -152,15 +149,14 @@ export function get_property_assignments_by_deduction( } > = {} - for (const structure of structures) { - grouped[structure.id] = { + for (const row of rows) { + const { property_id, structure_id, is_satisfied, is_deduced } = row + + grouped[structure_id] ??= { satisfied: { non_deduced: new Set(), deduced: new Set() }, unsatisfied: { non_deduced: new Set(), deduced: new Set() }, } - } - for (const row of rows) { - const { property_id, structure_id, is_satisfied, is_deduced } = row grouped[structure_id][is_satisfied ? 'satisfied' : 'unsatisfied'][ is_deduced ? 'deduced' : 'non_deduced' ].add(property_id) diff --git a/databases/catdat/scripts/utils/functors.ts b/databases/catdat/scripts/utils/functors.ts index 2a973148..0c935744 100644 --- a/databases/catdat/scripts/utils/functors.ts +++ b/databases/catdat/scripts/utils/functors.ts @@ -1,132 +1,45 @@ import { type Database } from 'better-sqlite3' import { parse_json_set } from './helpers' - -type FunctorMeta = { - id: string - name: string - associated_satisfied_properties: { - source: Set - target: Set - } -} - -type NormalizedFunctorImplication = { - id: string - assumptions: Set - conclusion: string - associated_assumptions: { - source: Set - target: Set - } -} +import type { StructureMeta } from './deduction' /** * Returns the list of functors saved in the database along with * the satisfied properties of their source and target category. */ -export function get_functors(db: Database): FunctorMeta[] { +export function get_functors(db: Database): StructureMeta[] { const rows = db - .prepare( + .prepare< + never[], + { + id: string + name: string + source: string + target: string + source_props: string + target_props: string + } + >( `SELECT id, name, source, target, ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_property_assignments - WHERE category_id = source AND is_satisfied = TRUE - ) + SELECT json_group_array(property_id) + FROM property_assignments + WHERE structure_id = source AND is_satisfied = TRUE ) as source_props, ( - SELECT json_group_array(property_id) FROM ( - SELECT property_id - FROM category_property_assignments - WHERE category_id = target AND is_satisfied = TRUE - ) + SELECT json_group_array(property_id) + FROM property_assignments + WHERE structure_id = target AND is_satisfied = TRUE ) as target_props - FROM functors + FROM functors_view ORDER BY lower(name)`, ) - .all() as { - id: string - name: string - source: string - target: string - source_props: string - target_props: string - }[] + .all() return rows.map((row) => ({ id: row.id, name: row.name, - associated_satisfied_properties: { - source: parse_json_set(row.source_props), - target: parse_json_set(row.target_props), - }, + source_props: parse_json_set(row.source_props), + target_props: parse_json_set(row.target_props), })) } - -/** - * Implications have the form - * P_1 + ... + P_n ===> Q_1 + ... + Q_m - * or - * P_1 + ... + P_n <===> Q_1 + ... + Q_m. - * This function decomposes them into normalized implications, - * which have the form - * P_1 + ... + P_n ===> Q. - */ -export function get_normalized_functor_implications( - db: Database, -): NormalizedFunctorImplication[] { - const all_implications_db = db - .prepare( - `SELECT - id, assumptions, source_assumptions, target_assumptions, - conclusions, is_equivalence - FROM functor_implications_view`, - ) - .all() as { - id: string - assumptions: string - source_assumptions: string - target_assumptions: string - conclusions: string - is_equivalence: 0 | 1 - }[] - - const implications: NormalizedFunctorImplication[] = [] - - for (const impl of all_implications_db) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - const source_assumptions = parse_json_set(impl.source_assumptions) - const target_assumptions = parse_json_set(impl.target_assumptions) - - for (const conclusion of conclusions) { - implications.push({ - id: impl.id, - assumptions, - conclusion, - associated_assumptions: { - source: source_assumptions, - target: target_assumptions, - }, - }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption, - associated_assumptions: { - source: source_assumptions, - target: target_assumptions, - }, - }) - } - } - } - - return implications -} diff --git a/databases/catdat/scripts/utils/helpers.ts b/databases/catdat/scripts/utils/helpers.ts index b5c34725..c17c3170 100644 --- a/databases/catdat/scripts/utils/helpers.ts +++ b/databases/catdat/scripts/utils/helpers.ts @@ -2,6 +2,7 @@ import Database, { type Database as DatabaseType } from 'better-sqlite3' import path from 'node:path' import fs from 'node:fs' import YAML from 'yaml' +import { StructureType } from '../config' export function are_equal_sets(a: Set, b: Set) { return a.size === b.size && [...a].every((el) => b.has(el)) @@ -22,6 +23,12 @@ export function parse_json_set(json: string): Set { return new Set(JSON.parse(json)) } +export const pluralize = (type: StructureType) => { + if (type == 'category') return 'categories' + if (type === 'functor') return 'functors' + throw new Error('Invalid type:', type) +} + export function get_client() { const db_path = path.resolve('databases', 'catdat', 'catdat.db') const db = new Database(db_path, { readonly: false }) diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index 1ca4613e..0f50d624 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/databases/catdat/scripts/utils/implications.ts @@ -1,7 +1,15 @@ import { type Database } from 'better-sqlite3' -import type { NormalizedImplication, PropertyMeta } from './deduction' -import { are_equal_sets, parse_json_set } from './helpers' +import type { PropertyMeta } from './deduction' import { StructureType } from '../config' +import { parse_json_set } from './helpers' + +export type NormalizedImplication = { + id: string + assumptions: Set + source_assumptions?: Set + target_assumptions?: Set + conclusion: string +} function get_assumption_string( implication: NormalizedImplication, @@ -10,6 +18,8 @@ function get_assumption_string( ): string { const { assumptions } = implication + // TODO: also incorporate source_assumptions and target_assumptions if present + return Array.from(assumptions) .map( (assumption) => @@ -61,49 +71,97 @@ export function get_contradiction_string( } /** - * Clears all deduced implications. This is done before the deduction starts. - */ -export function clear_deduced_implications(db: Database, type: StructureType) { - db.prepare(`DELETE FROM ${type}_implications WHERE is_deduced = TRUE`).run() -} - -type ImplicationWithDualProperties = { - assumptions: string - conclusions: string - dual_assumptions: string - dual_conclusions: string - dual_source_assumptions?: string - dual_target_assumptions?: string -} - -/** - * Checks if an implication can be dualized (i.e. if all the involved properties - * have a dual) and if the dual is different from it. + * Implications have the form + * P_1 + ... + P_n ===> Q_1 + ... + Q_m + * or + * P_1 + ... + P_n <===> Q_1 + ... + Q_m. + * This function decomposes them into normalized implications, + * which have the form + * P_1 + ... + P_n ===> Q_i. */ -export function is_dualizable(impl: ImplicationWithDualProperties): boolean { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - const dual_assumptions = parse_json_set(impl.dual_assumptions) - const dual_conclusions = parse_json_set(impl.dual_conclusions) - - if (dual_assumptions.has(null) || dual_conclusions.has(null)) return false - - if (impl.dual_source_assumptions) { - const dual_source_assumptions = parse_json_set( - impl.dual_source_assumptions, - ) - if (dual_source_assumptions.has(null)) return false - } - - if (impl.dual_target_assumptions) { - const dual_target_assumptions = parse_json_set( - impl.dual_target_assumptions, +export function get_normalized_functor_implications( + db: Database, + type: StructureType, +): NormalizedImplication[] { + const all_implications_db = db + .prepare< + [string], + { + id: string + is_equivalence: 0 | 1 + assumptions: string + source_assumptions: string + target_assumptions: string + conclusions: string + } + >( + `SELECT + i.id, + i.is_equivalence, + ( + SELECT json_group_array(property_id) + FROM implication_properties ip + WHERE ip.implication_id = i.id + AND ip.structure = 'self' + AND ip.kind = 'assumption' + ) as assumptions, + ( + SELECT json_group_array(property_id) + FROM implication_properties ip + WHERE ip.implication_id = i.id + AND ip.structure = 'source' + AND ip.kind = 'assumption' + ) as source_assumptions, + ( + SELECT json_group_array(property_id) + FROM implication_properties ip + WHERE ip.implication_id = i.id + AND ip.structure = 'target' + AND ip.kind = 'assumption' + ) as target_assumptions, + ( + SELECT json_group_array(property_id) + FROM implication_properties ip + WHERE ip.implication_id = i.id + AND ip.structure = 'self' + AND ip.kind = 'conclusion' + ) as conclusions + FROM implications i + WHERE i.type = ? + GROUP BY i.id`, ) - if (dual_target_assumptions.has(null)) return false + .all(type) + + const implications: NormalizedImplication[] = [] + + for (const impl of all_implications_db) { + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) + const source_assumptions = parse_json_set(impl.source_assumptions) + const target_assumptions = parse_json_set(impl.target_assumptions) + + for (const conclusion of conclusions) { + implications.push({ + id: impl.id, + assumptions, + conclusion, + ...(source_assumptions.size > 0 && { source_assumptions }), + ...(target_assumptions.size > 0 && { target_assumptions }), + }) + } + + if (impl.is_equivalence) { + for (const assumption of assumptions) { + implications.push({ + id: impl.id, + assumptions: conclusions, + conclusion: assumption, + ...(source_assumptions.size > 0 && { source_assumptions }), + ...(target_assumptions.size > 0 && { target_assumptions }), + }) + } + } } - return !( - are_equal_sets(assumptions, dual_assumptions) && - are_equal_sets(conclusions, dual_conclusions) - ) + return implications }