more blog post wip

.tokeignore

@@ -1,3 +1,4 @@
 public
 package-lock.json
 src/styles/fork-awesome
+pnpm-lock.yaml

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

@@ -14,7 +14,7 @@ draft: true
 <summary>Imports</summary>
 
 ```
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 module 2024-09-18-hcomp.index where
 open import Cubical.Foundations.Prelude hiding (isProp→isSet)
 open import Cubical.Foundations.Equiv.Base
@@ -33,6 +33,8 @@ 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:
 
+![](./2d.jpg)
+
 ```
 path-comp : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
 path-comp {x = x} p q i =
@@ -51,11 +53,13 @@ This result exists in the cubical standard library, but let's go over it here.
 
 ```
 isProp→isSet : {A : Type} → isProp A → isSet A
-isProp→isSet {A} A-isProp = goal where
+isProp→isSet {A} f = goal where
   goal : (x y : A) → (p q : x ≡ y) → p ≡ q
   goal x y p q j i = -- ...
 ```
 
+We're given a type $A$, some proof that it's a mere proposition, let's call it $f : \mathsf{isProp}(A)$.
+
 Now let's construct an hcomp. In a set, we'd want paths $p$ and $q$ between the same points $x$ and $y$ to be equal.
 Suppose $p$ and $q$ operate over the same dimension, $i$.
 If we want to find a path between $p$ and $q$, we'll want another dimension.
@@ -79,13 +83,18 @@ Before getting started, let's familiarize ourselves with the dimensions we're wo
 We can map both $p(i)$ and $q(i)$ down to a square that has $x$ on all corners and $\mathsf{refl}_x$ on all sides.
 
 Let's start with the left and right faces $(i = \{ \mathsf{i0} , \mathsf{i1} \})$.
-These can be produced using the $\mathsf{isProp}(A)$ that we are given.
+These can be produced using the proof $f : \mathsf{isProp}(A)$ that we are given.
-$\mathsf{isProp}(A)$ tells us that $x$ and $y$ are the same, so $x \equiv x$ and $x \equiv y$.
+$f$ tells us that $x$ and $y$ are the same, so $f(x, x) = x \equiv x$ and $f(x, y) = x \equiv y$.
-This means we can define the left face as $\mathsf{isProp}(A, x, x, k)$ and the right face as $\mathsf{isProp}(A, x, y, k)$.
+This means we can define the left face as $f(x, x, k)$ and the right face as $f(x, y, k)$.
 (Remember, $k$ is the direction going from bottom to top)
 
 ![](./sides.jpg)
 
+We can write this down as a mapping:
+
+* $(i = \mathsf{i0}) \rightarrow f(x, x, k)$
+* $(i = \mathsf{i1}) \rightarrow f(x, y, k)$
+
 Since $k$ is only the bottom-to-top dimension, the front-to-back dimension isn't changing.
 So we can use $\mathsf{refl}$ for those bottom edges.
 
@@ -102,10 +111,10 @@ Putting this all together, we can using $\mathsf{hcomp}$ to complete the top fac
 
 ```
     let u = λ k → λ where
-      (i = i0) → A-isProp x x k
+      (i = i0) → f x x k
-      (i = i1) → A-isProp x y k
+      (i = i1) → f x y k
-      (j = i0) → A-isProp x (p i) k
+      (j = i0) → f x (p i) k
-      (j = i1) → A-isProp x (q i) k
+      (j = i1) → f x (q i) k
     in hcomp u x
 ```
 
@@ -118,7 +127,10 @@ Let's move on to a more complicated example.
 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.
+![](./numberline.jpg)
+
+Since the $0$-sphere is just two points (solutions to $\| \bm{x} \|_2 = 1$ in 1 dimension), we represent this as $S^0 :\equiv 2$.
+We can show that a suspension over this, $\Sigma 2$, is equivalent to the classic $1$-sphere, the circle $S^1$.
 
 Let's state the lemma:
 
@@ -136,11 +148,23 @@ In this model, we're going to define $f$ and $g$ by having both the north and so
 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">
+Here's a picture of our function $f$:
-<tbody>
-<tr style="vertical-align: top">
 
-<td>
+![](./suspbool.jpg)
+
+The left setup is presented in the traditional suspension layout, with meridians going through $\mathsf{true}$ and $\mathsf{false}$ while the right side "squishes" the north and south poles using $\mathsf{refl}$, while having the other path represent the $\mathsf{loop}$.
+
+On the other side, $g$, we want to map back from $S^1$ into $\Sigma 2$.
+We can map the $\mathsf{loop}$ back into $\mathsf{merid} \; \mathsf{false}$, but the types mismatch, since $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$ but $\mathsf{merid} \; \mathsf{false} : \mathsf{north} \equiv \mathsf{south}$.
+But since $\mathsf{merid} \; \mathsf{true}$ is $\mathsf{refl}$, we can just concatenate with its inverse to get the full path:
+
+$$
+\mathsf{merid} \; \mathsf{false} \cdot (\mathsf{merid} \; \mathsf{true})^{-1} : \mathsf{north} \equiv \mathsf{north}
+$$
+
+In Agda, we can write it like this:
+
+<div class="halfSplit">
 
 ```
   f : Susp Bool → S¹
@@ -150,34 +174,24 @@ This way, $\mathsf{true}$ is suspended into the $\mathsf{refl}$ path, and $\math
   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>
+</div>
 
-</tr>
+Now, the fun part is to show the extra requirements that is needed to show that these two functions indeed form an isomorphism.
-</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}$.
+The base case is easily handled by $\mathsf{refl}$, since $f(g(\mathsf{base})) = f(\mathsf{north}) = \mathsf{base}$ definitionally by the reduction rules we gave above.
 
 ```
   fg : (s : S¹) → f (g s) ≡ s
   fg base = refl
 ```
 
-The loop case is trickier. Let's solve it algebraically first:
+The loop case is trickier. If we were using book HoTT, here's how we would solve this (this result is given in Lemma 6.5.1 of the HoTT book):
 
 $$
 \begin{align*}
@@ -191,21 +205,43 @@ $$
 \end{align*}
 $$
 
-Between the second and third steps, I used functoriality of the $\mathsf{ap}$ operation.
+Between the second and third steps, I used functoriality of the $\mathsf{ap}$ operation (equation _(i)_ of Lemma 2.2.2 in the HoTT book).
+
+How can we construct a cube to solve this? Like in the first example, let's start out by writing down the face we want to end up with:
+
+![](./goal2.jpg)
+
+We're looking for the path in the bottom-to-top $j$ dimension.
+We would like to have $\mathsf{hcomp}$ give us this face.
+This time, let's see the whole cube first and then pick apart how it was constructed.
+
+![](./fg.jpg)
+
+First of all, note that unrolling $f(g(\mathsf{loop} \; i))$ would give us $f((\mathsf{merid} \; \mathsf{false} \cdot (\mathsf{merid} \; \mathsf{true})^{-1}) \; i)$, which is the same as $f(\mathsf{merid} \; \mathsf{false} \; i) \cdot f(\mathsf{merid} \; \mathsf{true} \; (\sim i))$.
+Since this is a composition, it deserves its own face of the cube, with our goal $f(g(\mathsf{loop} \; i))$ being the lid.
+
+We can express this as an $\mathsf{hfill}$ operation, which is similar to $\mathsf{hcomp}$ in that it takes the same face arguments, but produces the contents of the face rather than just the upper lid.
+
+For the rest of the faces, we can just fill in opposite sides until the cube is complete.
+The Agda translation looks like this:
 
 ```
-  fg (loop i) k =
+  fg (loop i) j =
     let
-      u = λ j → λ where
+      u = λ k → λ where
         (i = i0) → base
-        (i = i1) → f (merid true (~ j))
+        (i = i1) → f (merid true (~ k))
-        (k = i0) → compPath-filler
+        (j = i0) →
-                      (λ i → f (merid false i))
+          let u = λ k' → λ where
-                      (λ j → f (merid true (~ j))) j i
+            (i = i0) → base
-        (k = i1) → loop i
+            (i = i1) → f (merid true (~ k'))
+          in hfill u (inS (f (merid false i))) k
+        (j = i1) → loop i
     in hcomp u (f (merid false i))
 ```
 
+Nothing should be too surprising here, other than the use of a nested $\mathsf{hfill}$ which is needed to describe the face that contains the composition.
+
 ```
   gf : (b : Susp Bool) → g (f b) ≡ b
   gf north = refl

src/styles/leftNav.scss

@@ -37,7 +37,7 @@
   }
 
   .portrait {
-    aspect-ratio: 1;
+    aspect-ratio: 1 / 1;
   }
 
   a.portrait {
@@ -47,8 +47,8 @@
 
   a.portrait img {
     border-radius: 100%;
-    width: 100%;
+    width: auto;
-    height: 100%;
+    height: auto;
   }
 
   .bio {

src/styles/post.scss

@@ -99,7 +99,7 @@
     p>img {
       margin: auto;
       max-width: 75%;
-      max-height: 240px;
+      max-height: 280px;
 
       width: auto;
       height: auto;
@@ -281,3 +281,18 @@ hr.endline {
     --admonition-bg-color: var(--warning-bg-color);
   }
 }
+
+.halfSplit {
+  display: flex;
+  flex-direction: row;
+  gap: 12px;
+  overflow-y: auto;
+
+  @media screen and (max-width: 960px) {
+    flex-direction: column;
+
+    pre.Agda {
+      margin: 0;
+    }
+  }
+}