From 5846dd5d043e708bad3db78823181e18cb286f80 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 1 Dec 2024 22:19:45 -0800 Subject: [PATCH] Fix typos Signed-off-by: Danila Fedorin --- content/blog/08_spa_agda_forward/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/blog/08_spa_agda_forward/index.md b/content/blog/08_spa_agda_forward/index.md index 3928e30..b2bb42b 100644 --- a/content/blog/08_spa_agda_forward/index.md +++ b/content/blog/08_spa_agda_forward/index.md @@ -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, \(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 -\(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 >}} f : (A \to L_2) \to (A \to L_2)