diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts
index 02b01fa..8e4c300 100644
--- a/plugin/remark-agda.ts
+++ b/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?",
);
diff --git a/src/content/posts/2024-09-18-hcomp/index.lagda.md b/src/content/posts/2024-09-18-hcomp/index.lagda.md
index f90c57d..85b6e99 100644
--- a/src/content/posts/2024-09-18-hcomp/index.lagda.md
+++ b/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
+
+
+Imports
```
{-# 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.
+
+
+## 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:
-Our goal is to find out what completes this square.
-Well, one way to complete a square is to treat it as the top face of a cube and use $\mathsf{hcomp}$.
+Our goal is to fill this square in.
+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}$.
+
+
+
+
+
+
+
+```
+ f : Susp Bool → S¹
+ f north = base
+ f south = base
+ f (merid true i) = base
+ f (merid false i) = loop i
+```
+
+
+
+
+
+```
+ g : S¹ → Susp Bool
+ g base = north
+ g (loop i) = (merid false ∙ sym (merid true)) i
+
+
+```
+
+
+
+
+
+
+
+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 = {! !}
+```