diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md
index 68bee16..98e0741 100644
--- a/content/blog/01_spa_agda_lattices.md
+++ b/content/blog/01_spa_agda_lattices.md
@@ -333,6 +333,7 @@ A lattice is made up of two semilattices. The operations of these two lattices,
 however, must satisfy some additional properties. Let's examine the properties
 in the context of `min` and `max` as we have before. They are usually called 
 the _absorption laws_:
+{#absorption-laws}
 
 * `max(a, min(a, b)) = a`. `a` is either less than or bigger than `b`;
   so if you try to find the maximum __and__ the minimum of `a` and
diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md
index 5af54e1..d120290 100644
--- a/content/blog/03_spa_agda_fixed_height.md
+++ b/content/blog/03_spa_agda_fixed_height.md
@@ -61,9 +61,10 @@ an infinite chain of map lattice elements in general:
 
 As long as we have infinite keys to choose from, we can always keep
 adding new keys to make bigger and bigger maps. But if we fix the keys in
-the map -- say, we use only `a` and `b` -- then suddenly our heights are once
+the map --- say, we use only `a` and `b` --- then suddenly our heights are once
 again fixed. In fact, for the two keys I just picked, one longest chain
 is remarkably similar to the product chain above.
+{#fin-keys}
 
 {{< latex >}}
 \{a: \bot, a: \bot\} < \{a: \bot, b: +\} < \{a: \bot, b: \top\} < \{a: +, b: \top\} < \{a: \top, b: \top\}
@@ -138,7 +139,7 @@ Thus, bringing the operators and other definitions of `IsLattice` into scope
 will also bring in the `FixedHeight` predicate.
 
 ### Fixed Height of the "Above-Below" Lattice
-We've already seen intuitive evidence that the sign lattice --- which is an instance of 
+We've already seen intuitive evidence that the sign lattice --- which is an instance of
 the ["above-below" lattice]({{< relref "01_spa_agda_lattices#the-above-below-lattice" >}}) ---
 has a fixed height. The reason is simple: we extended a set of incomparable
 elements with a single element that's greater, and a single element that's lower.
@@ -173,7 +174,7 @@ I use this witness to construct the two-`<` chain.
 
 {{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 339 340 >}}
 
-The proof that the length of two -- in terms of comparisons -- is the
+The proof that the length of two --- in terms of comparisons --- is the
 bound of all chains of `AboveBelow` elements requires systematically
 rejecting all longer chains. Informally, suppose you have a chain of
 three or more comparisons.
@@ -302,6 +303,251 @@ as well as the fact that they bound the combined chain.
 
 This completes the proof!
 
-{{< todo >}}
-The rest of this.
-{{< /todo >}}
+### Iterated Products
+
+The product lattice allows us to combine finite height lattices into a
+new finite height lattice. From there, we can use this newly lattice
+as a component of yet another product lattice. For instance, if we had
+\(L_1 \times L_2\), we can take a product of that with \(L_1\) again,
+and get \(L_1 \times (L_1 \times L_2)\). Since this also creates a
+finite-height lattice, we can repeat this process, and keep
+taking a product with \(L_1\), creating:
+
+{{< latex >}}
+\overbrace{L_1 \times ... \times L_1}^{n\ \text{times}} \times L_2.
+{{< /latex >}}
+
+I call this the _iterated product lattice_. Its significance will become
+clear shortly; in the meantime, let's prove that it is indeed a lattice
+(of finite height).
+To create an iterated product lattice, we still need two constituent
+lattices as input.
+
+{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 7 11 >}}
+
+{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 21 22 >}}
+
+At a high level, the proof goes by induction on the number of applications
+of the product. There's just one trick. I'd like to build up an `isLattice`
+instance even if `A` and `B` are not finite-height. That's because in
+that case, the iterated product is still a lattice, just not one with
+a finite height. On the other hand, the `isFiniteHeightLattice` proof
+requires the `isLattice` proof. Since we're building up by induction,
+that means that every recursive invocation of the function, we need
+to get the "partial" lattice instance and give it to the "partial" finite
+height lattice instance. When I implemented the inductive proof for
+`isLattice` independently from the (more specific) inductive proof
+of `isFiniteHeightLattice`, Agda could not unify the two `isLattice`
+instances (the "actual" one and the one that serves as witness
+for `isFiniteHeightLattice`). This led to some trouble and inconvenience,
+and so, I thought it best to build the two up together.
+
+To build up with the lattice instance and --- if possible --- the finite height
+instance, I needed to allow for the constituent lattices either finite
+or infinite. I supported this by defining a helper type:
+
+{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 34 40 >}}
+
+Then, I defined the "everything at once" type, in which, instead of
+a field for the proof of finite height, has a field that constructs
+this proof _if the necessary additional information is present_.
+
+{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 42 55 >}}
+
+Finally, the proof by induction. It's actually relatively long, so I'll
+include it as a collapsible block.
+
+{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 95 "" "**(Click here to expand the inductive proof)**" >}}
+
+### Fixed Height of the Map Lattice
+
+We saw above that [we can make a map lattice have a finite height if
+we fix its keys](#finite-keys). How does this work? Well, if the keys
+are always the same, we can think of such a map as just a tuple, with
+as many element as there are keys.
+
+{{< latex >}}
+\begin{array}{cccccc}
+  \{ & a: 1, & b: 2, & c: 3, & \} \\
+   &  & \iff &  & \\
+  ( & 1, & 2, & 3 & )
+\end{array}
+{{< /latex >}}
+
+This is why I introduced the [iterated product](#iterated-products) earlier;
+we can use them to construct the second lattice in the example above.
+I'll take one departure from that example, though: I'll "pad" the tuples
+with an additional unit element at the end. The unit type (denoted \(\top\))
+--- which has only a single element --- forms a finite height lattice trivially;
+I prove this in [an appendix below](#appendix-the-unit-lattice).
+Using this padding helps reduce the number of special cases; without the
+adding, the tuple definition might be something like the following:
+
+{{< latex >}}
+\text{tup}(A, k) =
+\begin{cases}
+\top & k = 0 \\
+A & k = 1 \\
+A \times \text{tup}(A, k - 1) & k > 1
+\end{cases}
+{{< /latex >}}
+
+On the other hand, if we were to allow the extra padding, we could drop
+the definition down to:
+
+{{< latex >}}
+\text{tup}(A, k) = \text{iterate}(t \mapsto A \times t, k, \bot) =
+\begin{cases}
+\top & k = 0 \\
+A \times \text{tup}(A, k - 1) & k > 0
+\end{cases}
+{{< /latex >}}
+
+And so, we drop from two to three cases, which means less proof work for us.
+The tough part is to prove that the two representations of maps --- the
+key-value list and the iterated product --- are equivalent. We will not
+have much trouble proving that they're both lattices (we did that last time,
+for both [products]({{< relref "02_spa_agda_combining_lattices#the-cartesian-product-lattice" >}}) and [maps]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}})). Instead, what we need to do is prove that
+the height of one lattice is the same as the height of the other. We prove
+this by providing something like an [isomorphism](https://mathworld.wolfram.com/Isomorphism.html):
+a pair of functions that convert between the two representations, and
+preserve the properties and relationships (such as \((\sqcup)\)) of lattice
+elements. In fact, list of the conversion functions' properties is quite
+extensive:
+
+{{< codelines "agda" "agda-spa/Isomorphism.agda" 22 33 "hl_lines=8-12">}}
+
+1. First, the functions must preserve our definition of equivalence. Thus,
+   if we convert two equivalent elements from the list representation to
+   the tuple representation, the resulting tuples should be equivalent as well.
+   The reverse must be true, too.
+2. Second, the functions must preserve the binary operations --- see also the definition
+   of a [homomorphism](https://en.wikipedia.org/wiki/Homomorphism#Definition).
+   Specifically, if \(f\) is a conversion function, then the following
+   should hold:
+
+   {{< latex >}}
+   f(a \sqcup b) \approx f(a) \sqcup f(b)
+   {{< /latex >}}
+
+   For the purposes of proving that equivalent maps have finite heights, it
+   turns out that this property need only hold for the join operator \((\sqcup)\).
+3. Finally, the functions must be inverses of each other. If you convert
+   list to a tuple, and then the tuple back into a list, the resulting
+   value should be equivalent to what we started with. In fact, they
+   need to be both "left" and "right" inverses, so that both \(f(g(x))\approx x\)
+   and \(g(f(x)) \approx x\).
+
+Given this, the high-level proof is in two parts:
+
+1. __Proving that a chain of the same height exists in the second (e.g., tuple)
+   lattice:__ To do this, we want to take the longest chain in the first
+   (e.g. key-value list) lattice, and convert it into a chain in the second.
+   The mechanism for this is not too hard to imagine: we just take the original
+   chain, and apply the conversion function to each element.
+
+   Intuitively, this works because of the structure-preserving properties
+   we required above. For instance (recall the
+   [definition of \((\leq)\) explained by Lars Huple](https://lars.hupel.info/topics/crdt/03-lattices/#there-), which in brief is \(a \leq b \triangleq a \sqcup b = b\)):
+
+   {{< latex >}}
+   \begin{align*}
+   a \leq b & \iff (\text{definition of less than})\\
+   a \sqcup b \approx b & \iff (\text{conversions preserve equivalence}) \\
+   f(a \sqcup b) \approx f(b) & \iff (\text{conversions distribute over binary operations}) \\
+   f(a) \sqcup f(b) \approx f(b) & \iff (\text{definition of less than}) \\
+   f(a) \leq f(b)
+   \end{align*}
+   {{< /latex >}}
+2. __Proving that longer chains can't exist in the second (e.g., tuple) lattice:__
+   we've already seen the mechanism to port a chain from one lattice to
+   another lattice, and we can use this same mechanism (but switching directions)
+   to go in reverse. If we do that, we can take a chain of questionable length
+   in the tuple lattice, port it back to the key-value map, and use the
+   (already known) fact that its chains are bounded to conclude the same
+   thing about the tuple chain.
+
+As you can tell, the chain porting mechanism is doing the heavy lifting here.
+It's relatively easy to implement given the conditions we've set on
+conversion functions, in both directions:
+
+{{< codelines "agda" "agda-spa/Isomorphism.agda" 51 63 >}}
+
+With that, we can prove the second lattice's finite height:
+
+{{< codelines "agda" "agda-spa/Isomorphism.agda" 65 72 >}}
+
+
+The conversion functions are also not too difficult to define. I give
+them below, but I refrain from showing proofs of the more involved
+properties (such as the fact that `from` and `to` are inverses, preserve
+equivalence, and distribute over join) here. You can view them by clicking
+the link at the top of the code block below.
+
+{{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 67 84 >}}
+
+Above, `FiniteValueMap ks` is the type of maps whose keys are fixed to
+`ks`; defined as follows:
+
+{{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 50 52 >}}
+
+Proving the remaining properties (which as I mentioned, I omit from
+the main body of the post) is sufficient to apply the isomorphism,
+proving that maps with finite keys are of a finite height.
+
+
+### Using the Finite Height Property
+
+Lattices having a finite height is a crucial property for the sorts of
+static program analyses I've been working to implement. 
+We can create functions that traverse "up" through the lattice,
+creating larger values each time. If these lattices are of a finite height,
+then the static analyses functions can only traverse "so high".
+Under certain conditions, this
+guarantees that our static analysis will eventually terminate with
+a [fixed point](https://mathworld.wolfram.com/FixedPoint.html). Pragmatically,
+this is a state in which running our analysis does not yield any more information.
+
+The way that the fixed point is found is called the _fixed point algorithm_.
+We'll talk more about this in the next post.
+
+{{< seriesnav >}}
+
+### Appendix: The Unit Lattice
+
+The unit lattice is a relatively boring one. I use the built-in unit type
+in Agda, which (perhaps a bit confusingly) is represented using the symbol `⊤`.
+It only has a single constructor, `tt`.
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 6 7 >}}
+
+The equivalence for the unit type is just propositional equality (we have
+no need to identify unequal values of `⊤`, since there is only one value).
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 17 25 >}}
+
+Both the join \((\sqcup)\) and meet \((\sqcap)\) operations are trivially defined;
+in both cases, they simply take two `tt`s and produce a new `tt`.
+Mathematically, one might write this as \((\text{tt}, \text{tt}) \mapsto \text{tt}\).
+In Agda:
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 30 34 >}}
+
+These operations are trivially associative, commutative, and idempotent.
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 39 46 >}}
+
+That's sufficient for them to be semilattices:
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 48 54 >}}
+
+The [absorption laws]({{< relref "01_spa_agda_lattices#absorption-laws" >}})
+are also trivially satisfied, which means that the unit type forms a lattice.
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 78 90 >}}
+
+Since there's only one element, it's not really possible to have chains
+that contain any more than one value. As a result, the height (in comparisons)
+of the unit lattice is zero.
+
+{{< codelines "agda" "agda-spa/Lattice/Unit.agda" 102 117 >}}