more wip

plugin/remark-agda.ts

@@ -36,8 +36,6 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
 
     const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
     const agdaOutDir = join(tempDir, "output");
-    const agdaOutFilename = parse(path).base.replace(/\.lagda.md/, ".md");
-    const agdaOutFile = join(agdaOutDir, agdaOutFilename);
     mkdirSync(agdaOutDir, { recursive: true });
 
     const childOutput = spawnSync(
@@ -164,6 +162,8 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
         idx += 1;
       });
     } catch (e) {
+      // TODO: Figure out a way to handle this correctly
+      // Possibly by diffing?
       console.log(
         "Mismatch in number of args. Perhaps there was an empty block?",
       );

src/content/posts/2024-09-18-hcomp/index.lagda.md

@@ -1,21 +1,37 @@
 ---
-title: Examples of hcomp
+title: Visual examples of hcomp
 slug: 2024-09-18-hcomp
 date: 2024-09-18T04:07:13-05:00
 tags: [hott, cubical]
 draft: true
 ---
 
-**hcomp** is a primitive operation in cubical type theory.
+**hcomp** is a primitive operation in [cubical type theory][cchm] that completes the _lid_ of an incomplete cube, given the bottom face and some number of side faces.
+
+[CCHM]: https://arxiv.org/abs/1611.02108
+
+<details>
+<summary>Imports</summary>
 
 ```
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module 2024-09-18-hcomp.index where
 open import Cubical.Foundations.Prelude hiding (isProp→isSet)
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Core.Primitives
+open import Cubical.HITs.Susp.Base
+open import Cubical.HITs.S1.Base
+open import Data.Bool.Base
 ```
 
-Intuitively, hcomp can be understood as the composition operation.
+</details>
+
+## Two-dimensional case
+
+In two dimensions, hcomp can be understood as the double-composition operation.
+"Single" composition (between two paths rather than three) is typically implemented as a double composition with the left leg as $\mathsf{refl}$.
+Without the double composition, this looks like:
 
 ```
 path-comp : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
@@ -26,6 +42,8 @@ path-comp {x = x} p q i =
   in hcomp u (p i)
 ```
 
+The `(i = i0)` case in this case is $\mathsf{refl}_x(j)$ which is definitionally equal to $x$.
+
 ## Example: $\mathsf{isProp}(A) \rightarrow \mathsf{isSet}(A)$
 
 Suppose we want to prove that all mere propositions (h-level 1) are sets (h-level 2).
@@ -46,8 +64,10 @@ So essentially, the final goal is a square with these boundaries:
 
 ![](./goal.jpg)
 
-Our goal is to find out what completes this square.
+Our goal is to fill this square in.
-Well, one way to complete a square is to treat it as the top face of a cube and use $\mathsf{hcomp}$.
+Well, what is a square but a missing face in a 3-dimensional cube?
+Let's draw out what this cube looks like, and then have $\mathsf{hcomp}$ give us the top face.
+Before getting started, let's familiarize ourselves with the dimensions we're working with:
 
 * $i$ is the left-right dimension, the one that $p$ and $q$ work over
 * $j$ is the dimension of our final path between $p \equiv q$.
@@ -93,4 +113,100 @@ Hooray! Agda is happy with this.
 
 Let's move on to a more complicated example.
 
-## Example: $\Sigma \mathbb{2} \rightarrow S^1$
+## Example: $\Sigma \mathbb{2} \simeq S^1$
+
+Suspensions are an example of a higher inductive type.
+It can be shown that spheres can be iteratively defined in terms of suspensions.
+
+Since the $0$-sphere is just two points (solutions to $\| \bm{x} \|_2 = 1$ in 1 dimension), we can show that a suspension over this is equivalent to the classic $1$-sphere, or the circle.
+
+Let's state the lemma:
+
+```
+Σ2≃S¹ : Susp Bool ≃ S¹
+```
+
+Equivalences can be generated from isomorphisms:
+
+```
+Σ2≃S¹ = isoToEquiv (iso f g fg gf) where
+```
+
+In this model, we're going to define $f$ and $g$ by having both the north and south poles be squished into one side.
+The choice of side is arbitrary, so I'll choose $\mathsf{true}$.
+This way, $\mathsf{true}$ is suspended into the $\mathsf{refl}$ path, and $\mathsf{false}$ is suspended into the $\mathsf{loop}$.
+
+<table style="width: 100%; border: none">
+<tbody>
+<tr style="vertical-align: top">
+
+<td>
+
+```
+  f : Susp Bool → S¹
+  f north = base
+  f south = base
+  f (merid true i) = base
+  f (merid false i) = loop i
+```
+
+</td>
+
+<td>
+
+```
+  g : S¹ → Susp Bool
+  g base = north
+  g (loop i) = (merid false ∙ sym (merid true)) i
+
+
+```
+
+</td>
+
+</tr>
+</tbody>
+</table>
+
+Now, the fun part is to show the isomorphisms.
+Starting with the first, let's show $f(g(s)) \equiv s$.
+The base case is easily handled by $\mathsf{refl}$.
+
+```
+  fg : (s : S¹) → f (g s) ≡ s
+  fg base = refl
+```
+
+The loop case is trickier. Let's solve it algebraically first:
+
+$$
+\begin{align*}
+\mathsf{ap}_f(\mathsf{ap}_g(\mathsf{loop})) &\equiv \mathsf{loop} \\
+\mathsf{ap}_f(\mathsf{merid} \; \mathsf{false} \cdot (\mathsf{merid} \; \mathsf{true})^{-1}) &\equiv \mathsf{loop} \\
+\mathsf{ap}_f(\mathsf{merid} \; \mathsf{false}) \cdot \mathsf{ap}_f (\mathsf{merid} \; \mathsf{true})^{-1} &\equiv \mathsf{loop} \\
+\mathsf{loop} \cdot \mathsf{ap}_f (\mathsf{merid} \; \mathsf{true})^{-1} &\equiv \mathsf{loop} \\
+\mathsf{loop} \cdot \mathsf{refl}^{-1} &\equiv \mathsf{loop} \\
+\mathsf{loop} \cdot \mathsf{refl} &\equiv \mathsf{loop} \\
+\mathsf{loop} &\equiv \mathsf{loop} \\
+\end{align*}
+$$
+
+Between the second and third steps, I used functoriality of the $\mathsf{ap}$ operation.
+
+```
+  fg (loop i) k =
+    let
+      leftFace = λ j → compPath-filler (λ i → f (merid false i)) (λ j → f (merid true (~ j))) j i
+
+      u = λ j → λ where
+        (i = i0) → base
+        (i = i1) → f (merid true (~ j))
+        (k = i0) → leftFace j
+        (k = i1) → loop i
+    in hcomp u (f (merid false i))
+```
+
+```
+  gf : (b : Susp Bool) → g (f b) ≡ b
+  gf b = {!   !}
+```