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

grammar
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2024-09-19 17:31:38 -05:00
parent 2d92966043
commit bc92b2184b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/content/posts/2024-09-18-hcomp/index.lagda.md
View file

@ -202,7 +202,7 @@ In Agda, we can write it like this:
</div> </div>
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$ * $f(g(s)) \equiv s$
* $g(f(b)) \equiv b$ * $g(f(b)) \equiv b$