wip

plugin/remark-agda.ts

@@ -52,21 +52,28 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
       {},
     );
 
-    if (childOutput.error || !existsSync(agdaOutFile)) {
+    // Locate output file
+    const directory = readdirSync(agdaOutDir);
+    const outputFilename = directory.find((name) => name.endsWith(".md"));
+
+    if (childOutput.status !== 0 || outputFilename === undefined) {
       throw new Error(
-        `Agda error:
+        `Agda output:
 
         Stdout:
         ${childOutput.stdout}
 
         Stderr:
-        ${childOutput.stderr}`,
+        ${childOutput.stderr}
+        `,
         {
           cause: childOutput.error,
         },
       );
     }
 
+    const outputFile = join(agdaOutDir, outputFilename);
+
     // // TODO: Handle child output
     // console.error("--AGDA OUTPUT--");
     // console.error(childOutput);
@@ -106,7 +113,7 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
 
     const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
 
-    const doc = readFileSync(agdaOutFile);
+    const doc = readFileSync(outputFile);
 
     // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
     const tree2 = fromMarkdown(doc);

src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/index.lagda.md

@@ -6,13 +6,23 @@ tags: [algebraic-topology, hott]
 draft: true
 ---
 
+<details>
+<summary>Imports</summary>
+
 ```
-{-# OPTIONS --cubical #-}
-open import Cubical.Foundations.Prelude
-open import Data.Nat
-open import Data.Bool
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+module 2024-09-15-circle-is-a-suspension-over-booleans.index where
+open import Cubical.Core.Primitives
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.HITs.S1.Base
+open import Data.Bool.Base
+open import Data.Nat.Base
 ```
 
+</details>
+
 One of the simpler yet still very interesting space in algebraic topology is the **circle**.
 Analytically, a circle can described as the set of all points that satisfy:
 
@@ -61,10 +71,6 @@ $$
 It would be nice to have an iterative definition of spheres; one that doesn't rely on us using our intuition to form new ones.
 Ideally, it would be a function $S^n : \mathbb{N} \rightarrow \mathcal{U}$, where we could plug in an $n$ of our choosing.
 
-```
-S_ : ℕ → Type
-```
-
 For an iterative definition, we'd like some kind of base case.
 What's the base case of spheres?
 What is a $0$-sphere?
@@ -73,12 +79,65 @@ If we take our original analytic definition of spheres and plug in $0$, we find
 The space of solutions is just a space with two elements!
 In other words, the type of booleans is actually the $0$-sphere, $S^0$.
 
-```
-S zero = Bool
-```
+![](./1.png)
 
 How about the iterative case? How can we take an $n$-sphere and get an $(n+1)$-sphere?
+This is where we need something called a _suspension_.
+
+Suspensions are a form of higher inductive type (HIT). It can be defined like this:
 
 ```
-S (suc n) = Bool
+data Susp (A : Type) : Type where
+  north : Susp A
+  south : Susp A
+  merid : A → north ≡ south
 ```
+
+Intuitively, you take the entirety of the type $A$, and imagine it as some kind of plane.
+Then, add two points, $\mathsf{north}$ and $\mathsf{south}$, to the top and bottom respectively.
+Now, each original point in $A$ defines a _path_ between $\mathsf{north}$ and $\mathsf{south}$.
+
+![](./susp.png)
+
+It may not be too obvious, but the circle $S^1$, can be represented as a suspension of the booleans $S^0$.
+This is presented as Theorem 6.5.1 in the [HoTT book]. I'll go over it briefly here.
+
+[hott book]: https://homotopytypetheory.org/book/
+
+The main idea is to consider the paths generated by both the $\mathsf{true}$ and the $\mathsf{false}$ points to add up to a single $\mathsf{loop}$.
+Here's a visual guide:
+
+![](./boolsusp.png)
+
+We can write functions going back and forth:
+
+```
+Σ2→S¹ : Susp Bool → S¹
+Σ2→S¹ north = base -- map the north point to the base point
+Σ2→S¹ south = base -- also map the south point to the base point
+Σ2→S¹ (merid false i) = loop i -- for the path going through false, let's map this to the loop
+Σ2→S¹ (merid true i) = base -- for the path going through true, let's map this to refl
+
+S¹→Σ2 : S¹ → Susp Bool
+S¹→Σ2 base = north
+S¹→Σ2 (loop i) = {!   !}
+```
+
+Now, to finish showing the equivalence, we need to prove that these functions concatenate into the identity in both directions:
+
+```
+rightInv : section Σ2→S¹ S¹→Σ2
+rightInv = {!   !}
+
+leftInv : retract Σ2→S¹ S¹→Σ2
+leftInv = {!   !}
+```
+
+And this gives us our equivalence!
+
+```
+Σ2≃S¹ : Susp Bool ≃ S¹
+Σ2≃S¹ = isoToEquiv (iso Σ2→S¹ S¹→Σ2 rightInv leftInv)
+```
+
+In fact, we can also show that the $2$-sphere is the suspension of the $1$-sphere.

src/pages/posts/[...slug].astro

@@ -7,6 +7,7 @@ import Timestamp from "../../components/Timestamp.astro";
 import { getImage } from "astro:assets";
 import TocWrapper from "../../components/TocWrapper.astro";
 import TagList from "../../components/TagList.astro";
+import portrait from "../../assets/self.png";
 
 export async function getStaticPaths() {
   const posts = await getCollection("posts");
@@ -22,7 +23,7 @@ const post = Astro.props;
 const { Content, remarkPluginFrontmatter, headings } = await post.render();
 const { title, toc, heroImage: heroImagePath, heroAlt, draft } = post.data;
 
-let heroImage;
+let heroImage = undefined;
 if (heroImagePath) {
   heroImage = await getImage({ src: heroImagePath });
 }
@@ -40,8 +41,16 @@ const excerpt = remarkPluginFrontmatter.excerpt?.replaceAll("\n", "");
   <meta slot="head" property="og:description" content={excerpt} />
   <meta slot="head" property="og:type" content="article" />
   <meta slot="head" property="og:locale" content="en_US" />
-  {heroImage && <meta slot="head" property="og:image" content={heroImage.src} />}
-  {heroAlt && <meta slot="head" property="og:image:alt" content={heroAlt} />}
+  {heroImage ?
+    <>
+      <meta slot="head" property="og:image" content={heroImage.src} />
+      {heroAlt && <meta slot="head" property="og:image:alt" content={heroAlt} />}
+    </>
+    :
+    <>
+      <meta slot="head" property="og:image" content={portrait.src} />
+    </>
+  }
 
   <meta slot="head" property="keywords" content={post.data.tags.join(", ")} />
   <meta slot="head" property="description" content={excerpt} />