new blog post

plugin/remark-agda.ts

@@ -8,6 +8,7 @@ import {
   mkdirSync,
   mkdtempSync,
   readFileSync,
+  existsSync,
   readdirSync,
   copyFileSync,
   writeFileSync,
@@ -35,6 +36,8 @@ 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(
@@ -44,18 +47,32 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
         `--html-dir=${agdaOutDir}`,
         "--highlight-occurrences",
         "--html-highlight=code",
-        "--allow-unsolved-metas",
         path,
       ],
       {},
     );
 
-    // TODO: Handle child output
+    if (childOutput.error || !existsSync(agdaOutFile)) {
-    console.error("--AGDA OUTPUT--");
+      throw new Error(
-    console.error(childOutput);
+        `Agda error:
-    console.error(childOutput.stdout?.toString());
+
-    console.error(childOutput.stderr?.toString());
+        Stdout:
-    console.error("--AGDA OUTPUT--");
+        ${childOutput.stdout}
+
+        Stderr:
+        ${childOutput.stderr}`,
+        {
+          cause: childOutput.error,
+        },
+      );
+    }
+
+    // // TODO: Handle child output
+    // console.error("--AGDA OUTPUT--");
+    // console.error(childOutput);
+    // console.error(childOutput.stdout?.toString());
+    // console.error(childOutput.stderr?.toString());
+    // console.error("--AGDA OUTPUT--");
 
     const referencedFiles = new Set();
     for (const file of readdirSync(agdaOutDir)) {
@@ -87,11 +104,9 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
       }
     }
 
-    const filename = parse(path).base.replace(/\.lagda.md/, ".md");
     const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
-    const fullOutputPath = join(agdaOutDir, filename);
 
-    const doc = readFileSync(fullOutputPath);
+    const doc = readFileSync(agdaOutFile);
 
     // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
     const tree2 = fromMarkdown(doc);

src/Prelude.agda

@@ -4,22 +4,24 @@ module Prelude where
 
 open import Agda.Primitive
 
-module 𝟘 where
+private
-  data ⊥ : Set where
+  variable
-  ¬_ : Set → Set
+    l : Level
-  ¬ A = A → ⊥
-open 𝟘 public
 
-module 𝟙 where
+data ⊥ : Set where
-  data ⊤ : Set where
+
+rec-⊥ : {A : Set} → ⊥ → A
+rec-⊥ ()
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+data ⊤ : Set where
   tt : ⊤
-open 𝟙 public
 
-module 𝟚 where
+data Bool : Set where
-  data Bool : Set where
   true : Bool
   false : Bool
-open 𝟚 public
 
 id : {l : Level} {A : Set l} → A → A
 id x = x
@@ -39,6 +41,19 @@ open Nat public
 infix 4 _≡_
 data _≡_ {l} {A : Set l} : (a b : A) → Set l where
   instance refl : {x : A} → x ≡ x
+{-# BUILTIN EQUALITY _≡_ #-}
+
+ap : {A B : Set l} → (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
+ap f refl = refl
+
+sym : {A : Set l} {x y : A} → x ≡ y → y ≡ x
+sym refl = refl
+
+trans : {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans refl refl = refl
+
+infixl 10 _∙_
+_∙_ = trans
 
 transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
   → (P : A → Set l₂)
@@ -72,3 +87,9 @@ _∘_ : {A B C : Set} (g : B → C) → (f : A → B) → A → C
 
 _∼_ : {A B : Set} (f g : A → B) → Set
 _∼_ {A} f g = (x : A) → f x ≡ g x
+
+postulate
+  funExt : {l : Level} {A B : Set l}
+    → {f g : A → B}
+    → ((x : A) → f x ≡ g x)
+    → f ≡ g

src/content/posts/2023-04-21-proving-true-from-false.lagda.md

@@ -1,5 +1,5 @@
 ---
-title: "Formally proving true ≢ false in cubical Agda"
+title: "Formally proving true ≢ false in Homotopy Type Theory with Agda"
 slug: "proving-true-from-false"
 date: 2023-04-21
 tags: ["type-theory", "agda"]
@@ -12,12 +12,7 @@ math: true
 These are some imports that are required for code on this page to work properly.
 
 ```agda
-{-# OPTIONS --cubical #-}
+open import Prelude
-open import Cubical.Foundations.Prelude
-open import Prelude hiding (_≢_; _≡_; refl; transport)
-infix 4 _≢_
-_≢_ : ∀ {A : Set} → A → A → Set
-x ≢ y  =  ¬ (x ≡ y)
 ```
 
 </details>
@@ -53,9 +48,8 @@ left side so it becomes judgmentally equal to the right:
 - suc (suc (suc zero))
 - 3
 
-However, in cubical Agda, naively using `refl` with the inverse statement
+However, in Agda, naively using `refl` with the inverse statement doesn't work.
-doesn't work. I've commented it out so the code on this page can continue to
+I've commented it out so the code on this page can continue to compile.
-compile.
 
 ```
 -- true≢false = refl
@@ -88,7 +82,7 @@ The strategy here is we define some kind of "type-map". Every time we see
 `false`, we'll map it to empty.
 
 ```
-bool-map : Bool → Type
+bool-map : Bool → Set
 bool-map true = ⊤
 bool-map false = ⊥
 ```
@@ -98,26 +92,29 @@ over a path (the path supposedly given to us as the witness that true ≢ false)
 will produce a function from the inhabited type we chose to the empty type!
 
 ```
-true≢false p = transport (λ i → bool-map (p i)) tt
+true≢false p = transport bool-map p tt
 ```
 
 I used `true` here, but I could equally have just used anything else:
 
 ```
-bool-map2 : Bool → Type
+bool-map2 : Bool → Set
 bool-map2 true = 1 ≡ 1
 bool-map2 false = ⊥
 
 true≢false2 : true ≢ false
-true≢false2 p = transport (λ i → bool-map2 (p i)) refl
+true≢false2 p = transport bool-map2 p refl
 ```
 
 ## Note on proving divergence on equivalent values
 
-Let's make sure this isn't broken by trying to apply this to something that's
+> [!NOTE]
-actually true:
+> Update: some of these have been commented out since regular Agda doesn't support higher inductive types
 
-```
+Let's make sure this isn't broken by trying to apply this to something that's
+actually true, like this higher inductive type:
+
+```text
 data NotBool : Type where
   true1 : NotBool
   true2 : NotBool
@@ -128,8 +125,7 @@ In this data type, we have a path over `true1` and `true2` that is a part of the
 definition of the `NotBool` type. Since this is an intrinsic equality, we can't
 map `true1` and `true2` to divergent types. Let's see what happens:
 
-```
+```text
-{-# NON_COVERING #-}
 notbool-map : NotBool → Type
 notbool-map true1 = ⊤
 notbool-map true2 = ⊥

src/content/posts/2024-06-26-agda-rendering.lagda.md

@@ -12,7 +12,7 @@ First off, a demonstration. Here's the code for function application over a path
 
 ```
 open import Agda.Primitive
-open import Prelude
+open import Prelude hiding (ap)
 
 ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
   → (f : A → B)

src/content/posts/2024-06-28-boolean-equivalences.lagda.md

@@ -1,5 +1,5 @@
 ---
-title: "Boolean equivalences"
+title: "Boolean equivalences in HoTT"
 slug: 2024-06-28-boolean-equivalences
 date: 2024-06-28T21:37:04.299Z
 tags: ["agda", "type-theory", "hott"]
@@ -15,25 +15,41 @@ $$
   (2 \simeq 2) \simeq 2
 $$
 
-This problem is exercise 2.13 of the [Homotopy Type Theory book][book]. If you
+> [!NOTE]
-are planning to attempt this problem, spoilers ahead!
+> This problem is exercise 2.13 of the [Homotopy Type Theory book][book]. If you
+> are planning to attempt this problem, spoilers ahead!
 
 [book]: https://homotopytypetheory.org/book/
 
 <small>The following line imports some of the definitions used in this post.</small>
 
 ```
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Prelude
+open Σ
 ```
 
 ## The problem explained
 
-With just the notation, the problem may not be clear.
+With just that notation, the problem may not be clear.
-$2$ represents the set with only 2 elements in it, which is the booleans. The
+$2$ represents the set with only two elements in it, which is the booleans. The
 elements of $2$ are $\textrm{true}$ and $\textrm{false}$.
-In this expression, $\simeq$ denotes [_homotopy equivalence_][1] between sets,
+
-which you can think of as an isomorphism.
+```
-For some function $f : A \rightarrow B$, we say that $f$ is an equivalence if:
+data 𝟚 : Set where
+  true : 𝟚
+  false : 𝟚
+```
+
+In the problem statement, $\simeq$ denotes [_homotopy equivalence_][1] between
+sets, which you can think of as basically a fancy isomorphism. For some
+function $f : A \rightarrow B$, we say that $f$ is an equivalence[^equivalence]
+if:
+
+[^equivalence]: There are other ways to define equivalences. As we'll show, an important
+property that is missed by this definition is that equivalences should be _mere
+propositions_. The reason why this definition falls short of that requirement is
+shown by Theorem 4.1.3 in the [HoTT book][book].
 
 [1]: https://en.wikipedia.org/wiki/Homotopy#Homotopy_equivalence
 
@@ -56,7 +72,7 @@ Then, the expression $2 \simeq 2$ simply expresses an equivalence between the
 boolean set to itself. Here's an example of a function that satisfies this equivalence:
 
 ```
-bool-id : Bool → Bool
+bool-id : 𝟚 → 𝟚
 bool-id b = b
 ```
 
@@ -74,9 +90,9 @@ bool-id-eqv = mkEquiv bool-id id-homotopy id-homotopy
 
 We can package these together into a single definition that combines the
 function along with proof of its equivalence properties using a dependent
-pair[^1]:
+pair[^dependent-pair]:
 
-[^1]: A dependent pair (or $\Sigma$-type) is like a regular pair $\langle x, y\rangle$, but where $y$ can depend on $x$.
+[^dependent-pair]: A dependent pair (or $\Sigma$-type) is like a regular pair $\langle x, y\rangle$, but where $y$ can depend on $x$.
   For example, $\langle x , \textrm{isPrime}(x) \rangle$.
   In this case it's useful since we can carry the equivalence information along with the function itself.
   This type is rather core to Martin-Löf Type Theory, you can read more about it [here][dependent-pair].
@@ -93,7 +109,7 @@ A ≃ B = Σ (A → B) (λ f → isEquiv f)
 This gives us an equivalence:
 
 ```
-bool-eqv : Bool ≃ Bool
+bool-eqv : 𝟚 ≃ 𝟚
 bool-eqv = bool-id , bool-id-eqv
 ```
 
@@ -106,7 +122,7 @@ equivalences between the boolean type and itself. Here is another possible
 definition:
 
 ```
-bool-neg : Bool → Bool
+bool-neg : 𝟚 → 𝟚
 bool-neg true = false
 bool-neg false = true
 ```
@@ -127,7 +143,7 @@ bool-neg-eqv = mkEquiv bool-neg neg-homotopy neg-homotopy
     neg-homotopy true = refl
     neg-homotopy false = refl
 
-bool-eqv2 : Bool ≃ Bool
+bool-eqv2 : 𝟚 ≃ 𝟚
 bool-eqv2 = bool-neg , bool-neg-eqv
 ```
 
@@ -147,6 +163,255 @@ That's where the main exercise statement comes in: "show that" $(2 \simeq 2)
 \simeq 2$, or in other words, find an inhabitant of this type.
 
 ```
-_ : (Bool ≃ Bool) ≃ Bool
+main-theorem : (𝟚 ≃ 𝟚) ≃ 𝟚
-_ = {!   !}
 ```
+
+How do we do this? Well, remember what it means to define an equivalence: first
+define a function, then show that it is an equivalence. Since equivalences are
+symmetrical, it doesn't matter which way we start first. I'll choose to first
+define a function $2 \rightarrow 2 \simeq 2$. This is fairly easy to do by
+case-splitting:
+
+```
+f : 𝟚 → (𝟚 ≃ 𝟚)
+f true = bool-eqv
+f false = bool-eqv2
+```
+
+This maps `true` to the equivalence derived from the identity function, and
+`false` to the function derived from the negation function.
+
+Now we need another function in the other direction. We can't case-split on
+functions, but we can certainly case-split on their output. Specifically, we can
+differentiate `id` from `neg` by their behavior when being called on `true`:
+
+- $\textrm{id}(\textrm{true}) :\equiv \textrm{true}$
+- $\textrm{neg}(\textrm{true}) :\equiv \textrm{false}$
+
+```
+g : (𝟚 ≃ 𝟚) → 𝟚
+g eqv = (fst eqv) true
+  -- same as this:
+  -- let (f , f-is-equiv) = eqv in f true
+```
+
+Hold on. If you know about the cardinality of functions, you'll observe that in
+the space of functions $f : 2 \rightarrow 2$, there are $2^2 = 4$ equivalence
+classes of functions. So if we mapped 4 functions into 2, how could this be
+considered an equivalence?
+
+A **key observation** here is that we're not mapping from all possible functions
+$f : 2 \rightarrow 2$. We're mapping functions $f : 2 \simeq 2$ that have
+already been proven to be equivalences. This means we can count on them to be
+structure-preserving, and can rule out cases like the function that maps
+everything to true, since it can't possibly have an inverse.
+
+We'll come back to this later.
+
+First, let's show that $g \circ f \sim \textrm{id}$. This one is easy, we can
+just case-split. Each of the cases reduces to something that is definitionally
+equal, so we can use `refl`.
+
+```
+g∘f : (g ∘ f) ∼ id
+g∘f true = refl
+g∘f false = refl
+```
+
+Now comes the complicated case: proving $f \circ g \sim \textrm{id}$.
+
+> [!NOTE]
+> Since Agda's comment syntax is `--`, the horizontal lines in the code below
+> are simply a visual way of separating out our proof premises from our proof
+> goals.
+
+```
+module f∘g-case where
+  goal :
+    (eqv : 𝟚 ≃ 𝟚)
+    --------------------
+    → f (g eqv) ≡ id eqv
+
+  f∘g : (f ∘ g) ∼ id
+  f∘g eqv = goal eqv
+```
+
+Now our goal is to show that for any equivalence $\textrm{eqv} : 2 \simeq 2$,
+applying $f ∘ g$ to it is the same as not doing anything. We can evaluate the
+$g(\textrm{eqv})$ a little bit to give us a more detailed goal:
+
+```
+  goal2 :
+    (eqv : 𝟚 ≃ 𝟚)
+    --------------------------
+    → f ((fst eqv) true) ≡ eqv
+
+  -- Solving goal with goal2, leaving us to prove goal2
+  goal eqv = goal2 eqv
+```
+
+The problem is if you think about equivalences as encoding some rich data about
+a function, converting it to a boolean and back is sort of like shoving it into
+a lower-resolution domain and then bringing it back. How can we prove that the
+equivalence is still the same equivalence, and as a result proving that there
+are only 2 possible equivalences?
+
+Note that the function $f$ ultimately still only produces 2 values. That means
+if we want to prove this, we can case-split on $f$'s output. In Agda, this uses
+a syntax known as [with-abstraction]:
+
+[with-abstraction]: https://agda.readthedocs.io/en/v2.6.4.3-r1/language/with-abstraction.html
+
+```
+  goal3 :
+    (eqv : 𝟚 ≃ 𝟚) → (b : 𝟚) → (p : fst eqv true ≡ b)
+    ------------------------------------------------
+    → f b ≡ eqv
+
+  -- Solving goal2 with goal3, leaving us to prove goal3
+  goal2 eqv with b ← (fst eqv) true in p = goal3 eqv b p
+```
+
+We can now case-split on $b$, which is the output of calling $f$ on the
+equivalence returned by $g$. This means that for the `true` case, we need to
+show that $f(b) = \textrm{bool-eqv}$ (which is based on `id`) is equivalent to
+the equivalence that generated the `true`.
+
+Let's start with the `id` case; we just need to show that for every equivalence
+$e$ where running the equivalence function on `true` also returned `true`, $e
+\equiv f(\textrm{true})$.
+
+Unfortunately, we don't know if this is true unless our equivalences are _mere
+propositions_, meaning if two functions are identical, then so are their
+equivalences.
+
+$$
+  \textrm{isProp}(P) :\equiv \prod_{x, y: P}(x \equiv y)
+$$
+
+<small>Definition 3.3.1 from the [HoTT book][book]</small>
+
+Applying this to $\textrm{isEquiv}(f)$, we get the property:
+
+$$
+  \sum_{f : A → B} \left( \prod_{e_1, e_2 : \textrm{isEquiv}(f)} e_1 \equiv e_2 \right)
+$$
+
+This proof is shown later in the book, so I will use it here directly without proof[^equiv-isProp]:
+
+[^equiv-isProp]: I haven't worked that far in the book yet, but this is shown in Theorem 4.2.13 in the [HoTT book][book].
+I might write a separate post about that when I get there, it seems like an interesting proof as well!
+
+```
+  postulate
+    equiv-isProp : {A B : Set}
+      → (e1 e2 : A ≃ B) → (Σ.fst e1 ≡ Σ.fst e2)
+      -----------------------------------------
+      → e1 ≡ e2
+```
+
+Now we're going to need our **key observation** that we made earlier, that
+equivalences must not map both values to a single one.
+This way, we can pin the behavior of the function on all inputs by just using
+its behavior on `true`, since its output on `false` must be _different_.
+
+We can use a proof that [$\textrm{true} \not\equiv \textrm{false}$][true-not-false] that I've shown previously.
+
+[true-not-false]: https://mzhang.io/posts/proving-true-from-false/
+
+```
+  true≢false : true ≢ false
+      -- read: true ≡ false → ⊥
+  true≢false p = bottom-generator p
+    where
+      map : 𝟚 → Set
+      map true = ⊤
+      map false = ⊥
+
+      bottom-generator : true ≡ false → ⊥
+      bottom-generator p = transport map p tt
+```
+
+Let's transform this into information about $f$'s output on different inputs:
+
+```
+  observation : (f : 𝟚 → 𝟚) → isEquiv f → f true ≢ f false
+                                 -- read: f true ≡ f false → ⊥
+  observation f (mkEquiv g f∘g g∘f) p =
+    let
+      -- Given p : f true ≡ f false
+      -- Proof strategy is to call g on it to get (g ∘ f) true ≡ (g ∘ f) false
+      -- Then, use our equivalence properties to reduce it to true ≡ false
+      -- Then, apply the lemma true≢false we just proved
+      step1 = ap g p
+      step2 = sym (g∘f true) ∙ step1 ∙ (g∘f false)
+      step3 = true≢false step2
+    in step3
+```
+
+For convenience, let's rewrite this so that it takes in an arbitrary $b$ and
+returns the version of the inequality we want:
+
+```
+  observation' : (f : 𝟚 → 𝟚) → isEquiv f → (b : 𝟚) → f b ≢ f (bool-neg b)
+                                                  -- ^^^^^^^^^^^^^^^^^^^^
+  observation' f eqv true p = observation f eqv p
+  observation' f eqv false p = observation f eqv (sym p)
+```
+
+Then, solving the `true` case is simply a matter of using function
+extensionality (functions are equal if they are point-wise equal) to show that
+just the function part of the equivalences are identical, and then using this
+property to prove that the equivalences must be identical as well.
+
+```
+  goal3 eqv true p = equiv-isProp bool-eqv eqv functions-equal
+    where
+      e = fst eqv
+
+      pointwise-equal : (x : 𝟚) → e x ≡ x
+      pointwise-equal true = p
+      pointwise-equal false with ef ← e false in eq = helper ef eq
+        where
+          helper : (ef : 𝟚) → e false ≡ ef → ef ≡ false
+          helper true eq = rec-⊥ (observation' e (snd eqv) false (eq ∙ sym p))
+          helper false eq = refl
+
+      -- NOTE: fst bool-eqv = id, definitionally
+      functions-equal : id ≡ e
+      functions-equal = sym (funExt pointwise-equal)
+```
+
+The `false` case is proved similarly.
+
+```
+  goal3 eqv false p = equiv-isProp bool-eqv2 eqv functions-equal
+    where
+      e = fst eqv
+
+      pointwise-equal : (x : 𝟚) → e x ≡ bool-neg x
+      pointwise-equal true = p
+      pointwise-equal false with ef ← e false in eq = helper ef eq
+        where
+          helper : (ef : 𝟚) → e false ≡ ef → ef ≡ true
+          helper true eq = refl
+          helper false eq = rec-⊥ (observation' e (snd eqv) true (p ∙ sym eq))
+
+      functions-equal : bool-neg ≡ e
+      functions-equal = sym (funExt pointwise-equal)
+```
+
+Putting this all together, we get the property we want to prove:
+
+```
+open f∘g-case
+
+-- main-theorem : (𝟚 ≃ 𝟚) ≃ 𝟚
+main-theorem = g , mkEquiv f g∘f f∘g
+```
+
+Now that Agda's all happy, our work here is done!
+
+Going through all this taught me a lot about how the basics of equivalences and
+how to express a lot of different ideas into the type system. Thanks for
+reading!