ENH: Add double theory for diagrammatic equations (unary ops only).

ToposInstitute · Nov 13, 2024 · 4adf813 · 4adf813
1 parent 8fa3120
commit 4adf813
Show file tree

Hide file tree

Showing 3 changed files with 57 additions and 3 deletions.
diff --git a/package.json b/package.json
@@ -24,5 +24,5 @@
         "tsx": "^4.16.5",
         "typedoc": "^0.26.5"
     },
-    "packageManager": "pnpm@9.11.0"
+    "packageManager": "pnpm@9.12.3"
 }
diff --git a/packages/frontend/src/diagram/diagram_editor.tsx b/packages/frontend/src/diagram/diagram_editor.tsx
@@ -41,8 +41,8 @@ export default function DiagramPage() {
         const { doc } = liveDoc;
         invariant(doc.type === "diagram", () => `Expected diagram, got type: ${doc.type}`);
 
-        const modelReactiveDoc = await getLiveDoc<ModelDocument>(rpc, repo, doc.modelRef.refId);
-        const liveModel = enlivenModelDocument(doc.modelRef.refId, modelReactiveDoc, theories);
+        const modelLiveDoc = await getLiveDoc<ModelDocument>(rpc, repo, doc.modelRef.refId);
+        const liveModel = enlivenModelDocument(doc.modelRef.refId, modelLiveDoc, theories);
 
         return enlivenDiagramDocument(refId, liveDoc, liveModel);
     });

diff --git a/packages/frontend/src/stdlib/theories.tsx b/packages/frontend/src/stdlib/theories.tsx
@@ -436,3 +436,57 @@ stdTheories.add(
         });
     },
 );
+
+stdTheories.add(
+    {
+        id: "diagrammatic-equations",
+        name: "Equational theory",
+        description: "Systems of equations specified diagrammatically",
+        group: "Applied Mathematics",
+    },
+    (meta) => {
+        const thCategory = new catlog.ThCategory();
+        return new Theory({
+            ...meta,
+            theory: thCategory.theory(),
+            modelTypes: [
+                {
+                    tag: "ObType",
+                    obType: { tag: "Basic", content: "Object" },
+                    name: "Type",
+                    description: "Type of quantity",
+                    shortcut: ["Q"],
+                },
+                {
+                    tag: "MorType",
+                    morType: {
+                        tag: "Hom",
+                        content: { tag: "Basic", content: "Object" },
+                    },
+                    name: "Operation",
+                    description: "Arithmetical operation or differential operator",
+                    shortcut: ["A"],
+                },
+            ],
+            instanceTypes: [
+                {
+                    tag: "ObType",
+                    obType: { tag: "Basic", content: "Object" },
+                    name: "Quantity",
+                    description: "Variables and other numerical quantities",
+                    shortcut: ["Q"],
+                },
+                {
+                    tag: "MorType",
+                    morType: {
+                        tag: "Hom",
+                        content: { tag: "Basic", content: "Object" },
+                    },
+                    name: "Application",
+                    description: "Apply an operation to quantities",
+                    shortcut: ["A"],
+                },
+            ],
+        });
+    },
+);