From bc92b2184bed11546e96ec0f0a37b959302159e0 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 19 Sep 2024 17:31:38 -0500 Subject: [PATCH] grammar --- src/content/posts/2024-09-18-hcomp/index.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/content/posts/2024-09-18-hcomp/index.lagda.md b/src/content/posts/2024-09-18-hcomp/index.lagda.md index 4cdc9b9..21597c4 100644 --- a/src/content/posts/2024-09-18-hcomp/index.lagda.md +++ b/src/content/posts/2024-09-18-hcomp/index.lagda.md @@ -202,7 +202,7 @@ In Agda, we can write it like this: -Now, the fun part is to show the extra requirements that is needed to show that these two functions indeed form an isomorphisms: +Now, the fun part is to show the extra requirements that are needed to show that these two functions indeed form an isomorphism: * $f(g(s)) \equiv s$ * $g(f(b)) \equiv b$