diff --git a/.tokeignore b/.tokeignore index 04849f7..698f6c8 100644 --- a/.tokeignore +++ b/.tokeignore @@ -1,3 +1,4 @@ public package-lock.json -src/styles/fork-awesome \ No newline at end of file +src/styles/fork-awesome +pnpm-lock.yaml diff --git a/src/content/posts/2024-09-18-hcomp/2d.jpg b/src/content/posts/2024-09-18-hcomp/2d.jpg new file mode 100644 index 0000000..308def1 Binary files /dev/null and b/src/content/posts/2024-09-18-hcomp/2d.jpg differ diff --git a/src/content/posts/2024-09-18-hcomp/fg.jpg b/src/content/posts/2024-09-18-hcomp/fg.jpg new file mode 100644 index 0000000..750c2f5 Binary files /dev/null and b/src/content/posts/2024-09-18-hcomp/fg.jpg differ diff --git a/src/content/posts/2024-09-18-hcomp/goal2.jpg b/src/content/posts/2024-09-18-hcomp/goal2.jpg new file mode 100644 index 0000000..eb189f4 Binary files /dev/null and b/src/content/posts/2024-09-18-hcomp/goal2.jpg differ 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 bdaff64..12adc4e 100644 --- a/src/content/posts/2024-09-18-hcomp/index.lagda.md +++ b/src/content/posts/2024-09-18-hcomp/index.lagda.md @@ -14,7 +14,7 @@ draft: true Imports ``` -{-# 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. -$\mathsf{isProp}(A)$ tells us that $x$ and $y$ are the same, so $x \equiv x$ and $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)$. +These can be produced using the proof $f : \mathsf{isProp}(A)$ that we are given. +$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 $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 = i1) → A-isProp x y k - (j = i0) → A-isProp x (p i) k - (j = i1) → A-isProp x (q i) k + (i = i0) → f x x k + (i = i1) → f x y k + (j = i0) → f x (p 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}$. - - - +Here's a picture of our function $f$: - - - + - - -
+![](./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: + +
``` 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 ``` -
 - ``` 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. +Now, the fun part is to show the extra requirements that is needed to show that these two functions indeed form an isomorphism. 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)) - (k = i0) → compPath-filler - (λ i → f (merid false i)) - (λ j → f (merid true (~ j))) j i - (k = i1) → loop i + (i = i1) → f (merid true (~ k)) + (j = i0) → + let u = λ k' → λ where + (i = i0) → base + (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 diff --git a/src/content/posts/2024-09-18-hcomp/numberline.jpg b/src/content/posts/2024-09-18-hcomp/numberline.jpg new file mode 100644 index 0000000..b73b52a Binary files /dev/null and b/src/content/posts/2024-09-18-hcomp/numberline.jpg differ diff --git a/src/content/posts/2024-09-18-hcomp/suspbool.jpg b/src/content/posts/2024-09-18-hcomp/suspbool.jpg new file mode 100644 index 0000000..59709df Binary files /dev/null and b/src/content/posts/2024-09-18-hcomp/suspbool.jpg differ diff --git a/src/styles/leftNav.scss b/src/styles/leftNav.scss index 500d44a..e16b56b 100644 --- a/src/styles/leftNav.scss +++ b/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%; - height: 100%; + width: auto; + height: auto; } .bio { diff --git a/src/styles/post.scss b/src/styles/post.scss index 51d19e9..d94323a 100644 --- a/src/styles/post.scss +++ b/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; @@ -280,4 +280,19 @@ hr.endline { --admonition-color: var(--warning-color); --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; + } + } } \ No newline at end of file