fix

package.json

@@ -15,7 +15,7 @@
     "@astrojs/markdoc": "^0.11.1",
     "@astrojs/markdown-remark": "^5.1.1",
     "@astrojs/mdx": "^1.1.5",
-    "@astrojs/rss": "^3.0.0",
+    "@astrojs/rss": "^4.0.7",
     "@astrojs/sitemap": "^3.1.6",
     "@justfork/rehype-autolink-headings": "^5.1.1",
     "astro": "^3.6.5",

plugin/remark-typst.ts

@@ -1,39 +1,55 @@
 import type { RemarkPlugin } from "@astrojs/markdown-remark";
 import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
 import { visit } from "unist-util-visit";
-import { join } from "node:path";
+import { join, resolve, dirname } from "node:path";
 import { spawnSync } from "node:child_process";
 import { tmpdir } from "node:os";
+import { readdir, copyFile } from "node:fs/promises";
 
 const remarkTypst: RemarkPlugin = () => {
   const tmp = mkdtempSync(join(tmpdir(), "typst"));
   let ctr = 0;
 
-  return (tree) => {
+  return async (tree, { history }) => {
+    const path: string = resolve(history[history.length - 1]!);
+    const dir = dirname(path);
+
+    // Copy all the .typ files in the dir
+    for (const file of await readdir(dir)) {
+      console.log("checking", file);
+      if (file.endsWith(".typ")) {
+        const src = resolve(join(dir, file));
+        const dst = resolve(join(tmp, file));
+        console.log("copying", src, dst);
+        await copyFile(src, dst);
+      }
+    }
+
     visit(
       tree,
       (node) => node.type === "code" && node.lang === "typst",
       (node, index, parent) => {
-        const doc = join(tmp, `${ctr}.typ`);
+        const doc = resolve(join(tmp, `${ctr}.typ`));
-        const docOut = join(tmp, `${ctr}.svg`);
+        const docOut = resolve(join(tmp, `${ctr}.svg`));
         ctr += 1;
 
         writeFileSync(doc, node.value);
-        const result = spawnSync(
+        const result = spawnSync("typst", [
-          "typst",
+          "compile",
-          [
+          "--format",
-            "compile",
+          "svg",
-            "--format",
+          doc,
-            "svg",
+          docOut,
-            doc,
+        ]);
-          ],
-          {},
-        );
         console.log("OUTPUT", result.stderr.toString());
 
         const svgOut = readFileSync(docOut);
         node.type = "html";
-        node.value = svgOut.toString();
+        node.value = `
+          <div class="svg">
+            ${svgOut.toString()}
+          </div>
+        `;
       },
     );
   };

pnpm-lock.yaml

@@ -18,8 +18,8 @@ importers:
         specifier: ^1.1.5
         version: 1.1.5(astro@3.6.5(@types/node@20.14.9)(sass@1.77.6))
       '@astrojs/rss':
-        specifier: ^3.0.0
+        specifier: ^4.0.7
-        version: 3.0.0
+        version: 4.0.7
       '@astrojs/sitemap':
         specifier: ^3.1.6
         version: 3.1.6
@@ -163,8 +163,8 @@ packages:
     resolution: {integrity: sha512-Z9IYjuXSArkAUx3N6xj6+Bnvx8OdUSHA8YoOgyepp3+zJmtVYJIl/I18GozdJVW1p5u/CNpl3Km7/gwTJK85cw==}
     engines: {node: ^18.17.1 || ^20.3.0 || >=21.0.0}
 
-  '@astrojs/rss@3.0.0':
+  '@astrojs/rss@4.0.7':
-    resolution: {integrity: sha512-PMX8iqByk9gtOrusikten/oF5uHjOCZigL6RuXFBUu+xtdKQxXzfIohJ99V2haA4FJjVDyibDTGzXR81POBMxQ==}
+    resolution: {integrity: sha512-ZEG55XFB19l+DplUvBISmz04UbjDtKliRO4Y5+ERRhAMjgCVVobEBNE6ZwWG1h6orWUocy4nfPihKXDyB73x9g==}
 
   '@astrojs/sitemap@3.1.6':
     resolution: {integrity: sha512-1Qp2NvAzVImqA6y+LubKi1DVhve/hXXgFvB0szxiipzh7BvtuKe4oJJ9dXSqaubaTkt4nMa6dv6RCCAYeB6xaQ==}
@@ -3344,7 +3344,7 @@ snapshots:
     dependencies:
       prismjs: 1.29.0
 
-  '@astrojs/rss@3.0.0':
+  '@astrojs/rss@4.0.7':
     dependencies:
       fast-xml-parser: 4.4.0
       kleur: 4.1.5

src/content/posts/2024-09-26-glue/arrow.typ

@@ -0,0 +1,11 @@
+#import "@preview/fletcher:0.5.1" as fletcher: diagram, node, edge
+
+#let arrow(left, right, leftcolor: red, rightcolor: blue) = diagram(cell-size: 1cm, $
+    #text(fill: leftcolor)[#left]
+    edge(
+      marks: #(none, (inherit: "head", stroke: rightcolor)),
+      stroke: #stroke(paint: gradient.linear(leftcolor, rightcolor))
+    )
+    &
+    #text(fill: rightcolor)[#right]
+  $)

src/content/posts/2024-09-26-glue/index.lagda.md

@@ -0,0 +1,76 @@
+---
+title: Glue
+slug: 2024-09-26-glue
+date: 2024-09-26T21:24:18.030Z
+tags: [hott, cubical, agda, type-theory]
+draft: true
+---
+
+<details>
+<summary>Imports for Agda</summary>
+
+```
+{-# OPTIONS --cubical #-}
+
+module 2024-09-26-glue.index where
+
+open import Cubical.Foundations.Prelude
+```
+
+</details>
+
+The core idea behind cubical type theory is that we have powerful path primitives that give us the ability to just bridge arbitrary things together.
+The $\mathsf{PathP}$ primitive gives us a way to connect elements of different types.
+
+For example, let's create some custom boolean type and assume we have some path between it and the standard booleans:
+
+```
+module _ where
+  data Bool : Type where
+    false : Bool
+    true : Bool
+
+  data Direction : Type where
+    left : Direction
+    right : Direction
+
+  postulate
+    myFunnyPath1 : Bool ≡ Direction
+```
+
+At the point $\mathsf{i0}$, this is _definitionally_ equal to $\mathsf{Bool}$,
+and at $\mathsf{i1}$, this is _definitionally_ equal to $\mathsf{Direction}$.
+
+```
+  _ : myFunnyPath1 i0 ≡ Bool
+  _ = refl
+
+  _ : myFunnyPath1 i1 ≡ Direction
+  _ = refl
+```
+
+These are known as the _boundary conditions_ on the path $\mathsf{myFunnyPath1}$.
+
+Not only this, we can provide paths between the elements of this type too:
+
+```
+  postulate
+    myFunnyPath2 : PathP (λ i → myFunnyPath1 i) false left
+```
+
+There's definitely something funny going on here. The typical transport operations in homotopy type theory are defined using path induction, which is inherent from the inductive structure of paths.
+But how do we perform path induction on this kind of path?
+
+Cubical type theory's approach is to flip this around and make _transport_ the primitive operation on top of which path induction can be defined.
+
+$$
+\mathsf{transp} : (A : \mathbb{I} \rightarrow \mathcal{U}) \rightarrow (r : \mathbb{I}) \rightarrow A(\mathsf{i0}) \rightarrow A(\mathsf{i1})
+$$
+
+Computationally, you could imagine how the path above would be transported:
+
+```typst
+#set page(width: auto, height: auto, margin: 10pt)
+#import "arrow.typ": arrow
+#arrow($C$, $D$, leftcolor: green)
+```

src/pages/index.astro

@@ -7,6 +7,8 @@ import "../styles/home.scss";
 const currentUrl = Astro.url;
 ---
 
+<link rel="alternate" type="application/rss+xml" href="/rss.xml" title="RSS Feed" slot="head" />
+
 <BaseLayout>
   <h1>Blog</h1>
 

src/styles/post.scss

@@ -108,6 +108,17 @@
       border: 1px solid var(--hr-color);
     }
 
+    .svg {
+      display: flex;
+      flex-direction: column;
+      align-items: center;
+
+      svg {
+        width: auto;
+        height: auto;
+      }
+    }
+
     details {
       border: 1px solid var(--hr-color);
       border-radius: 8px;
@@ -295,4 +306,4 @@ hr.endline {
       margin: 0;
     }
   }
-}
+}