From bbfe4f67ca104d43a0fb675e8b125f68b8ab4a9c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 29 Jun 2024 15:15:42 -0500 Subject: [PATCH] More updates --- .../posts/2024-06-28-boolean-equivalences.lagda.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) 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 9d18995..0835cb6 100644 --- a/src/content/posts/2024-06-28-boolean-equivalences.lagda.md +++ b/src/content/posts/2024-06-28-boolean-equivalences.lagda.md @@ -15,9 +15,10 @@ $$ (2 \simeq 2) \simeq 2 $$ -> [!NOTE] -> This problem is exercise 2.13 of the [Homotopy Type Theory book][book]. If you -> are planning to attempt this problem, spoilers ahead! +> [!admonition: WARNING] +> :warning: This post describes exercise 2.13 of the [Homotopy Type Theory +> book][book]. If you are planning to attempt this problem yourself, spoilers +> ahead! [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}$. -> [!NOTE] +> [!admonition: 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. @@ -411,6 +412,6 @@ 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 +Going through all this taught me a lot about how the basics of equivalences work +and how to express a lot of different ideas into the type system. Thanks for reading!