diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md
index af43f97..a6d9bad 100644
--- a/content/blog/02_spa_agda_combining_lattices.md
+++ b/content/blog/02_spa_agda_combining_lattices.md
@@ -16,7 +16,7 @@ of variables in a program.
 
 At the end of that post, I introduced a source of complexity: the "full"
 lattices that we want to use for the program analysis aren't signs or numbers,
-but maps of states and variables to lattices-based states. The full lattice
+but maps of states and variables to lattice-based descriptions. The full lattice
 for sign analysis might something in the form:
 
 {{< latex >}}
@@ -25,12 +25,12 @@ for sign analysis might something in the form:
 
 Thus, we have to compare and find least upper bounds (e.g.) of not just
 signs, but maps! Proving the various lattice laws for signs was not too
-challenging, but for for a two-level map like \(\text{info}\) above, we'd
-need to do a lot more work. We need tools to build up such complicated lattices!
+challenging, but for for a two-level map like \(\text{Info}\) above, we'd
+need to do a lot more work. We need tools to build up such complicated lattices.
 
 The way to do this, it turns out, is by using simpler lattices as building blocks.
 To start with, let's take a look at a very simple way of combining lattices:
-taking the Cartesian product.
+taking the [Cartesian product](https://mathworld.wolfram.com/CartesianProduct.html).
 
 ### The Cartesian Product Lattice
 
@@ -39,12 +39,13 @@ post, each lattice comes equipped with a "least upper bound" operator \((\sqcup)
 and a "greatest lower bound" operator \((\sqcap)\). Since we now have two lattices,
 let's use numerical suffixes to disambiguate between the operators
 of the first and second lattice: \((\sqcup_1)\) will be the LUB operator of
-the first lattice \(L_1\), and \((\sqcup_2)\) of the second lattice \(L_2\).
+the first lattice \(L_1\), and \((\sqcup_2)\) of the second lattice \(L_2\),
+and so on.
 
 Then, let's take the Cartesian product of the elements of \(L_1\) and \(L_2\);
 mathematically, we'll write this as \(L_1 \times L_2\), and in Agda, we can
 just use the standard [`Data.Product`](https://agda.github.io/agda-stdlib/master/Data.Product.html)
-module. In Agda, I'll define the lattice as another [parameterized module](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules). Since both \(L_1\) and \(L_2\)
+module. Then, I'll define the lattice as another [parameterized module](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules). Since both \(L_1\) and \(L_2\)
 are lattices, this parameterized module will require `IsLattice` instances
 for both types:
 
@@ -52,7 +53,7 @@ for both types:
 
 Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where
 \(l_1 \in L_1\) and \(l_2 \in L_2\). The first thing we can get out of the
-way is define what it means for two such elements to be equal. Recall that
+way is defining what it means for two such elements to be equal. Recall that
 we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitional-equality" >}})
 instead of definitional equality to allow similar elements to be considered
 equal; we'll have to define a similar relation for our new product lattice.
@@ -75,7 +76,7 @@ relations.
 
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 42 48 >}}
 
-In fact, defining \((\sqcup)\) and \((\sqcap)\) by simply applying the
+Defining \((\sqcup)\) and \((\sqcap)\) by simply applying the
 corresponding operators from \(L_1\) and \(L_2\) seems quite natural as well.
 
 {{< latex >}}
@@ -88,8 +89,8 @@ In Agda:
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 50 54 >}}
 
 All that's left is to prove the various (semi)lattice properties. Intuitively,
-we can see that since the "combined" operator `_≈_` just independently applies
-the element operators `_≈₁_` and `_≈₂_`, as long as they are idempotent,
+we can see that since the "combined" operator `_⊔_` just independently applies
+the element operators `_⊔₁_` and `_⊔₂_`, as long as they are idempotent,
 commutative, and associative, so is the "combined" operator itself.
 Moreover, the proofs that `_⊔_` and `_⊓_` form semilattices are identical
 up to replacing \((\sqcup)\) with \((\sqcap)\). Thus, in Agda, we can write
@@ -98,8 +99,9 @@ that these operators obey the semilattice laws).
 
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 56 82 >}}
 
-Similarly to the semilattice properties, proving lattice properties boils
-down to applying the lattice properties of \(L_1\) and \(L_2\) to
-individual components.
+Above, I used `f₁` to stand for "either `_⊔₁_` or `_⊓₁_`", and similarly
+`f₂` for "either `_⊔₂_` or `_⊓₂_`". Much like the semilattice properties,
+proving lattice properties boils down to applying the lattice properties of
+\(L_1\) and \(L_2\) to individual components.
 
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 84 96 >}}