diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts index 762fc05..8714e57 100644 --- a/plugin/remark-agda.ts +++ b/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); diff --git a/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/1.png b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/1.png new file mode 100644 index 0000000..53ecb80 Binary files /dev/null and b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/1.png differ diff --git a/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/boolsusp.png b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/boolsusp.png new file mode 100644 index 0000000..7559023 Binary files /dev/null and b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/boolsusp.png differ diff --git a/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans.lagda.md b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/index.lagda.md similarity index 50% rename from src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans.lagda.md rename to src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/index.lagda.md index d5d5c8a..93016ea 100644 --- a/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans.lagda.md +++ b/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 --- +
+Imports + ``` -{-# 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 ``` +
+ 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. diff --git a/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/susp.png b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/susp.png new file mode 100644 index 0000000..d2752c5 Binary files /dev/null and b/src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/susp.png differ diff --git a/src/pages/posts/[...slug].astro b/src/pages/posts/[...slug].astro index 7d8d9e0..30a3673 100644 --- a/src/pages/posts/[...slug].astro +++ b/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", ""); - {heroImage && } - {heroAlt && } + {heroImage ? + <> + + {heroAlt && } + + : + <> + + + }