diff --git a/bun.lockb b/bun.lockb
index 6bda38a..0ed914a 100755
Binary files a/bun.lockb and b/bun.lockb differ
diff --git a/package.json b/package.json
index 43a8072..518889f 100644
--- a/package.json
+++ b/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",
diff --git a/plugin/remark-typst.ts b/plugin/remark-typst.ts
index 2c8b7dd..2a5ce23 100644
--- a/plugin/remark-typst.ts
+++ b/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 docOut = join(tmp, `${ctr}.svg`);
+ const doc = resolve(join(tmp, `${ctr}.typ`));
+ const docOut = resolve(join(tmp, `${ctr}.svg`));
ctr += 1;
writeFileSync(doc, node.value);
- const result = spawnSync(
- "typst",
- [
- "compile",
- "--format",
- "svg",
- doc,
- ],
- {},
- );
+ const result = spawnSync("typst", [
+ "compile",
+ "--format",
+ "svg",
+ doc,
+ docOut,
+ ]);
console.log("OUTPUT", result.stderr.toString());
const svgOut = readFileSync(docOut);
node.type = "html";
- node.value = svgOut.toString();
+ node.value = `
+
+ ${svgOut.toString()}
+
+ `;
},
);
};
diff --git a/src/content/posts/2024-09-26-glue/arrow.typ b/src/content/posts/2024-09-26-glue/arrow.typ
new file mode 100644
index 0000000..3dd5588
--- /dev/null
+++ b/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]
+ $)
diff --git a/src/content/posts/2024-09-26-glue/index.lagda.md b/src/content/posts/2024-09-26-glue/index.lagda.md
new file mode 100644
index 0000000..9432ada
--- /dev/null
+++ b/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
+---
+
+
+Imports for Agda
+
+```
+{-# OPTIONS --cubical #-}
+
+module 2024-09-26-glue.index where
+
+open import Cubical.Foundations.Prelude
+```
+
+
+
+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)
+```
diff --git a/src/styles/post.scss b/src/styles/post.scss
index d94323a..13e8193 100644
--- a/src/styles/post.scss
+++ b/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;
}
}
-}
\ No newline at end of file
+}