Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix typos

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-12-01 22:19:45 -08:00
parent f6b347eb05
commit 5846dd5d04
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
content/blog/08_spa_agda_forward/index.md
View File

@ -207,7 +207,7 @@ At first, the exercise may not obviously correspond to the bulk operation
I've described. Particularly confusing is the fact that it has two lattices, I've described. Particularly confusing is the fact that it has two lattices,
\(L_1\) and \(L_2\). In fact, the exercise results in a very general theorem; \(L_1\) and \(L_2\). In fact, the exercise results in a very general theorem;
we can exploit a more concrete version of the theorem by setting we can exploit a more concrete version of the theorem by setting
\(L_1 \triangleq A \to L_2\), resulting in an overal signature for \(f\) and \(h\): \(L_1 \triangleq A \to L_2\), resulting in an overall signature for \(f\) and \(h\):
{{< latex >}} {{< latex >}}
f : (A \to L_2) \to (A \to L_2) f : (A \to L_2) \to (A \to L_2)