diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts
index fd987d2..762fc05 100644
--- a/plugin/remark-agda.ts
+++ b/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
- console.error("--AGDA OUTPUT--");
- console.error(childOutput);
- console.error(childOutput.stdout?.toString());
- console.error(childOutput.stderr?.toString());
- console.error("--AGDA OUTPUT--");
+ if (childOutput.error || !existsSync(agdaOutFile)) {
+ throw new Error(
+ `Agda error:
+
+ Stdout:
+ ${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);
diff --git a/src/Prelude.agda b/src/Prelude.agda
index cbda14a..1a48425 100644
--- a/src/Prelude.agda
+++ b/src/Prelude.agda
@@ -4,22 +4,24 @@ module Prelude where
open import Agda.Primitive
-module π where
- data β₯ : Set where
- Β¬_ : Set β Set
- Β¬ A = A β β₯
-open π public
+private
+ variable
+ l : Level
-module π where
- data β€ : Set where
- tt : β€
-open π public
+data β₯ : Set where
-module π where
- data Bool : Set where
- true : Bool
- false : Bool
-open π public
+rec-β₯ : {A : Set} β β₯ β A
+rec-β₯ ()
+
+Β¬_ : Set β Set
+Β¬ A = A β β₯
+
+data β€ : Set where
+ tt : β€
+
+data Bool : Set where
+ true : Bool
+ false : Bool
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
diff --git a/src/content/posts/2023-04-21-proving-true-from-false.lagda.md b/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
index ce40566..920d783 100644
--- a/src/content/posts/2023-04-21-proving-true-from-false.lagda.md
+++ b/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 Cubical.Foundations.Prelude
-open import Prelude hiding (_β’_; _β‘_; refl; transport)
-infix 4 _β’_
-_β’_ : β {A : Set} β A β A β Set
-x β’ y = Β¬ (x β‘ y)
+open import Prelude
```
@@ -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
-doesn't work. I've commented it out so the code on this page can continue to
-compile.
+However, in Agda, naively using `refl` with the inverse statement doesn't work.
+I've commented it out so the code on this page can continue to 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
-actually true:
+> [!NOTE]
+> 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:
-```
-{-# NON_COVERING #-}
+```text
notbool-map : NotBool β Type
notbool-map true1 = β€
notbool-map true2 = β₯
diff --git a/src/content/posts/2024-06-26-agda-rendering.lagda.md b/src/content/posts/2024-06-26-agda-rendering.lagda.md
index 61f9e6d..89a03f4 100644
--- a/src/content/posts/2024-06-26-agda-rendering.lagda.md
+++ b/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)
diff --git a/src/content/posts/2024-06-28-boolean-equivalences.lagda.md b/src/content/posts/2024-06-28-boolean-equivalences.lagda.md
index 68525f6..5543792 100644
--- a/src/content/posts/2024-06-28-boolean-equivalences.lagda.md
+++ 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
-are planning to attempt this problem, spoilers ahead!
+> [!NOTE]
+> 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/
The following line imports some of the definitions used in this post.
```
+{-# OPTIONS --allow-unsolved-metas #-}
open import Prelude
+open Ξ£
```
## The problem explained
-With just the notation, the problem may not be clear.
-$2$ represents the set with only 2 elements in it, which is the booleans. The
+With just that notation, the problem may not be clear.
+$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)
+$$
+
+Definition 3.3.1 from the [HoTT book][book]
+
+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!