michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

More updates

Browse source
This commit is contained in:
Michael Zhang 2024-06-29 15:15:42 -05:00
parent 9318880a9a
commit bbfe4f67ca
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -15,9 +15,10 @@ $$
(2 \simeq 2) \simeq 2 (2 \simeq 2) \simeq 2
$$ $$
> [!NOTE] > [!admonition: WARNING]
> This problem is exercise 2.13 of the [Homotopy Type Theory book][book]. If you > :warning: This post describes exercise 2.13 of the [Homotopy Type Theory
> are planning to attempt this problem, spoilers ahead! > book][book]. If you are planning to attempt this problem yourself, spoilers
> ahead!
[book]: https://homotopytypetheory.org/book/ [book]: https://homotopytypetheory.org/book/
@ -219,7 +220,7 @@ g∘f false = refl
Now comes the complicated case: proving $f \circ g \sim \textrm{id}$. Now comes the complicated case: proving $f \circ g \sim \textrm{id}$.
> [!NOTE] > [!admonition: NOTE]
> Since Agda's comment syntax is `--`, the horizontal lines in the code below > 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 > are simply a visual way of separating out our proof premises from our proof
> goals. > goals.
@ -411,6 +412,6 @@ main-theorem = g , mkEquiv f g∘f f∘g
Now that Agda's all happy, our work here is done! 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 Going through all this taught me a lot about how the basics of equivalences work
how to express a lot of different ideas into the type system. Thanks for and how to express a lot of different ideas into the type system. Thanks for
reading! reading!