From 043b3ebe74b723051c92a664078ed438856b0b42 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 28 Jun 2024 20:48:21 -0500 Subject: [PATCH] new blog post --- plugin/remark-agda.ts | 35 ++- src/Prelude.agda | 49 ++- ...023-04-21-proving-true-from-false.lagda.md | 34 +- .../posts/2024-06-26-agda-rendering.lagda.md | 2 +- .../2024-06-28-boolean-equivalences.lagda.md | 297 +++++++++++++++++- 5 files changed, 357 insertions(+), 60 deletions(-) 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!