From 531b33442df60e2a02db1aeea9e5faa13328a246 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 28 Jun 2024 17:46:08 -0500 Subject: [PATCH] boolean equivalences --- plugin/remark-agda.ts | 1 + src/Prelude.agda | 23 +++ .../2024-06-28-boolean-equivalences.lagda.md | 152 ++++++++++++++++++ 3 files changed, 176 insertions(+) create mode 100644 src/content/posts/2024-06-28-boolean-equivalences.lagda.md diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts index cae42c3..fd987d2 100644 --- a/plugin/remark-agda.ts +++ b/plugin/remark-agda.ts @@ -44,6 +44,7 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => { `--html-dir=${agdaOutDir}`, "--highlight-occurrences", "--html-highlight=code", + "--allow-unsolved-metas", path, ], {}, diff --git a/src/Prelude.agda b/src/Prelude.agda index 47c781d..cbda14a 100644 --- a/src/Prelude.agda +++ b/src/Prelude.agda @@ -49,3 +49,26 @@ transport {l₁} {l₂} {A} {x} {y} P refl = id infix 4 _≢_ _≢_ : ∀ {A : Set} → A → A → Set x ≢ y = ¬ (x ≡ y) + +module dependent-product where + infixr 4 _,_ + infixr 2 _×_ + + record Σ {l₁ l₂} (A : Set l₁) (B : A → Set l₂) : Set (l₁ ⊔ l₂) where + constructor _,_ + field + fst : A + snd : B fst + open Σ + {-# BUILTIN SIGMA Σ #-} + syntax Σ A (λ x → B) = Σ[ x ∈ A ] B + + _×_ : {l : Level} (A B : Set l) → Set l + _×_ A B = Σ A (λ _ → B) +open dependent-product public + +_∘_ : {A B C : Set} (g : B → C) → (f : A → B) → A → C +(g ∘ f) a = g (f a) + +_∼_ : {A B : Set} (f g : A → B) → Set +_∼_ {A} f g = (x : A) → f x ≡ g x diff --git a/src/content/posts/2024-06-28-boolean-equivalences.lagda.md b/src/content/posts/2024-06-28-boolean-equivalences.lagda.md new file mode 100644 index 0000000..68525f6 --- /dev/null +++ b/src/content/posts/2024-06-28-boolean-equivalences.lagda.md @@ -0,0 +1,152 @@ +--- +title: "Boolean equivalences" +slug: 2024-06-28-boolean-equivalences +date: 2024-06-28T21:37:04.299Z +tags: ["agda", "type-theory", "hott"] +draft: true +--- + +This post is about a problem I recently proved that seemed simple going in, but +I struggled with it for quite a while. The problem statement is as follows: + +Show that: + +$$ + (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! + +[book]: https://homotopytypetheory.org/book/ + +The following line imports some of the definitions used in this post. + +``` +open import Prelude +``` + +## 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 +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: + +[1]: https://en.wikipedia.org/wiki/Homotopy#Homotopy_equivalence + +- there exists a $g : B \rightarrow A$ +- $f \circ g$ is homotopic to the identity map $\textrm{id}_B : B \rightarrow B$ +- $g \circ f$ is homotopic to the identity map $\textrm{id}_A : A \rightarrow A$ + +We can write this in Agda like this: + +``` +record isEquiv {A B : Set} (f : A → B) : Set where + constructor mkEquiv + field + g : B → A + f∘g : (f ∘ g) ∼ id + g∘f : (g ∘ f) ∼ id +``` + +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 b = b +``` + +We can prove that it satisfies the equivalence, by giving it an inverse function +(itself), and proving that the inverse is homotopic to identity (which is true +definitionally): + +``` +bool-id-eqv : isEquiv bool-id +bool-id-eqv = mkEquiv bool-id id-homotopy id-homotopy + where + id-homotopy : (bool-id ∘ bool-id) ∼ id + id-homotopy _ = refl +``` + +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]: + +[^1]: 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]. + +[dependent-pair]: https://en.wikipedia.org/wiki/Dependent_type#%CE%A3_type + +``` +_≃_ : (A B : Set) → Set +A ≃ B = Σ (A → B) (λ f → isEquiv f) +``` + +Hint: (click the $\Sigma$ to see how it's defined!) + +This gives us an equivalence: + +``` +bool-eqv : Bool ≃ Bool +bool-eqv = bool-id , bool-id-eqv +``` + +Great! Now what? + +## The space of equivalences + +Turns out, the definition I gave above is just _one_ of multiple possible +equivalences between the boolean type and itself. Here is another possible +definition: + +``` +bool-neg : Bool → Bool +bool-neg true = false +bool-neg false = true +``` + +The remarkable thing about this is that nothing is changed by flipping true and +false. Someone using booleans would not be able to tell if you gave them a +boolean type where true and false were flipped. Simply put, the constructors +true and false are simply names and nothing can distinguish them. + +We can show this by proving that `bool-neg` also forms an equivalence by using +itself as the inverse. + +``` +bool-neg-eqv : isEquiv bool-neg +bool-neg-eqv = mkEquiv bool-neg neg-homotopy neg-homotopy + where + neg-homotopy : (bool-neg ∘ bool-neg) ∼ id + neg-homotopy true = refl + neg-homotopy false = refl + +bool-eqv2 : Bool ≃ Bool +bool-eqv2 = bool-neg , bool-neg-eqv +``` + +You could imagine more complicated functions over booleans that may also exhibit +this equivalence property. So how many different elements of the type $2 \simeq +2$ exist? + +## Proving $2 \simeq 2$ only has 2 inhabitants + +It turns out there are only 2 equivalences, the 2 that we already found. But how +do we know this for a fact? Well, if there are only 2 equivalences, that means +there are only 2 inhabitants of the type $2 \simeq 2$. We can prove that this +type only has 2 inhabitants by establishing an equivalence between this type and +another type that is known to have 2 inhabitants, such as the boolean type! + +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 +_ = {! !} +```