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)