From 37d59e69278b67b45b771bc81a52743dde615891 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 18 Sep 2024 06:01:37 -0500 Subject: [PATCH] more wip --- plugin/remark-agda.ts | 4 +- .../posts/2024-09-18-hcomp/index.lagda.md | 128 +++++++++++++++++- 2 files changed, 124 insertions(+), 8 deletions(-) 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: ![](./goal.jpg) -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 = {! !} +```