diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md
index c324f5f..4412a17 100644
--- a/content/blog/02_spa_agda_combining_lattices.md
+++ b/content/blog/02_spa_agda_combining_lattices.md
@@ -425,7 +425,7 @@ we can create the infinite chain:
 
 On the other hand, our sign lattice _is_ of finite height; the longest chains
 we can make have three elements and two `<` signs. Here's one:
-{#sign-length-three}
+{#sign-three-elements}
 
 {{< latex >}}
 \bot < + < \top
diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md
index ba11c1b..5af54e1 100644
--- a/content/blog/03_spa_agda_fixed_height.md
+++ b/content/blog/03_spa_agda_fixed_height.md
@@ -21,8 +21,8 @@ infinitely long:
 There isn't a "biggest natural number"! On the other hand, we've seen that our
 [sign lattice]({{< relref "01_spa_agda_lattices#sign-lattice" >}}) has a finite
 height; the longest chain we can make is three elements long; I showed one
-such chain (there are many chains of length three) in
-[the previous post]({{< relref "02_spa_agda_combining_lattices#sign-length-three" >}}),
+such chain (there are many chains of three elements) in
+[the previous post]({{< relref "02_spa_agda_combining_lattices#sign-three-elements" >}}),
 but here it is again:
 
 {{< latex >}}
@@ -38,11 +38,13 @@ chains have five elements. The following is one example:
 {{< latex >}}
 (\bot, \bot) < (\bot, +) < (\bot, \top) < (+, \top) < (\top, \top)
 {{< /latex >}}
+{#sign-prod-chain}
 
 The fact that \(L_1\) and \(L_2\) are themselves finite-height lattices is
 important; if either one of them is not, we can easily construct an infinite
 chain of the products. If we allowed \(L_2\) to be natural numbers, we'd
 end up with infinite chains like this one:
+{#product-both-finite-height}
 
 {{< latex >}}
 (\bot, 0) < (\bot, 1) < (\bot, 2) < ...
@@ -76,6 +78,230 @@ talk about them in a subsequent post.
 In the meantime, let's dig deeper into the notion of finite height, and
 the Agda proofs of the properties I've introduced thus far.
 
+### Formalizing Finite Height
+
+The formalization I settled on is quite similar to the informal description:
+a lattice has a finite height of length \(h\) if the longest chain
+of elements compared by \((<)\) is exactly \(h\). There's only a slight
+complication: we allow for equivalent-but-not-equal elements in lattices.
+For instance, for a map lattice, we don't care about the order of the keys:
+so long as two maps relate the same set of keys to the same respective values,
+we will consider them equal. This, however, is beyond the notion of Agda's
+propositional equality (`_≡_`). Thus, we we need to generalize the definition
+of a chain to support equivalences. I parameterize the `Chain` module
+in my code by an equivalence relation, as well as the comparison relation `R`,
+which we will set to `<` for our chains. The equivalence relation and `R`/`<`
+are expected to play together nicely (if `a < b`, and `a` is equivalent to `c`,
+then it should be the case that `c < b`).
+
+{{< codelines "agda" "agda-spa/Chain.agda" 3 7 >}}
+
+From there, the definition of the `Chain` data type is much like the definition
+of a vector, but indexed by the endpoints, and containing witnesses of `R`/`<`
+between its elements. The indexing allows for representing
+the type of chains between particular lattice elements, and serves to ensure
+concatenation and other operations don't merge disparate chains.
+
+{{< codelines "agda" "agda-spa/Chain.agda" 19 21 >}}
+
+In the `done` case, we create a single-element chain, which has no comparisons.
+In this case, the chain starts and stops at the same element (where "the same"
+is modulo our equivalence). The `step` case prepends a new comparison `a1 < a2`
+to an existing chain; once again, we allow for the existing chain to start
+with a different-but-equivalent element `a2'`.
+
+With that definition in hand, I define what it means for a type of
+chains between elements of the lattice `A` to have a maximum height; simply
+put, all chains must have length less than or equal to the maximum.
+
+{{< codelines "agda" "agda-spa/Chain.agda" 38 39 >}}
+
+Though `Bounded` specifies _a_ bound on the length of chains, it doesn't
+specify _the_ (lowest) bound. Specifically, if the chains can only have
+length three, they are bounded by both 3, 30, and 300. To claim a lowest
+bound, we need to show that a chain of that length actually exists (otherwise,
+we could take the previous natural number, and it would be a bound as well).
+Thus, I define the `Height` predicate to require that a chain of the desired
+height exists, and that this height bounds the length of all other chains.
+
+{{< codelines "agda" "agda-spa/Chain.agda" 47 48 >}}
+
+Finally, for a lattice to have a finite height, the type of chains formed by using
+its less-than operator needs to have that height (satisfy the `Height h` predicate).
+To avoid having to thread through the equivalence relation, congruence proof,
+and more, I define a specialized predicate for lattices specifically.
+I do so as a "method" in my `IsLattice` record.
+
+{{< codelines "agda" "agda-spa/Lattice.agda" 153 180 "hl_lines = 27 28">}}
+
+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 
+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.
+We can't make chains out of incomparable elements (since we can't compare them
+using `<`); thus, we can only have one `<` from the new least element, and
+one `<` from the new greatest element.
+
+The proof is a bit tedious, but not all that complicated.
+First, a few auxiliary helpers; feel free to read only the type signatures.
+They specify, respectively:
+1. That the bottom element \(\bot\) of the above-below lattice is less than any
+   concrete value from the underlying set. For instance, in the sign lattice case, \(\bot < +\).
+2. That \(\bot\) is the only element satisfying the first property; that is,
+   any value strictly less than an element of the underlying set must be \(\bot\).
+3. That the top element \(\top\) of the above-below lattice is greater than
+   any concrete value of the underlying set. This is the dual of the first property.
+4. That, much like the bottom element is the only value strictly less than elements
+   of the underlying set, the top element is the only value strictly greater.
+
+{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 315 335 >}}
+
+From there, we can construct an instance of the longest chain. Actually,
+there's a bit of a hang-up: what if the underlying set is empty? Concretely,
+what if there were no signs? Then we could only construct a chain with
+one comparison: \(\bot < \top\). Instead of adding logic to conditionally
+specify the length, I simply require that the set is populated by requiring
+a witness
+
+{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 85 85 >}}
+
+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
+bound of all chains of `AboveBelow` elements requires systematically
+rejecting all longer chains. Informally, suppose you have a chain of
+three or more comparisons.
+
+1. If it starts with \(\top\), you can't add any more elements since that's the
+   greatest element (contradiction).
+2. If you start with an element of the underlying set, you could add another
+   element, but it has to be the top element; after that, you can't add any
+   more (contradiction).
+3. If you start with \(\bot\), you could arrive at a chain of two comparisons,
+   but you can't go beyond that (in three cases, each leading to contradictions).
+
+{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 342 355 "hl_lines=8-14">}}
+
+Thus, the above-below lattice has a length of two comparisons (or alternatively,
+three elements).
+
+{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}}
+
+And that's it.
+
+### Fixed Height of the Product Lattice
+
+Now, for something less tedious. We saw above that for a product lattice
+to have a finite height,
+[its constituent lattices must have a finite height](#product-both-finite-height).
+The proof was by contradiction (by constructing an infinitely long product
+chain given a single infinite lattice). As a result, we'll focus this
+section on products of two finite lattices `A` and `B`. Additionally, for the
+proofs in this section, I require element equivalence to be decidable.
+
+{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 115 117 >}}
+
+Let's think about how we might go about constructing the longest chain in
+a product lattice. Let's start with some arbitrary element \(p_1 = (a_1, b_1)\).
+We need to find another value that isn't equal to \(p_1\), because we'rebuilding
+chains of the less-than operator \((<)\), and not the less-than-or-equal operator
+\((\leq)\). As a result, we need to change either the first component, the second
+component, or both.  If we're building "to the right" (adding bigger elements),
+the new components would need to be bigger. Suppose then that we came up
+with \(a_2\) and \(b_2\), with \(a_1 < a_2\) and \(b_1 < b_2\). We could then
+create a length-one chain:
+
+{{< latex >}}
+(a_1, b_1) < (a_2, b_2)
+{{< /latex >}}
+
+That works, but we can construct an even longer chain by increasing only one
+element at a time:
+
+{{< latex >}}
+(a_1, b_1) < (a_1, b_2) < (a_2, b_2)
+{{< /latex >}}
+
+We can apply this logic every time; the conclusion is that when building
+up a chain, we need to increase one element at a time. Then, how many times
+can we increase an element? Well, if lattice `A` has a height of two (comparisons),
+then we can take its lowest element, and increase it twice. Similarly, if
+lattice `B` has a height of three, starting at its lowest element, we can
+increase it three times. In all, when building a chain of `A × B`, we can
+increase an element five times.
+
+This gives us a recipe for constructing
+the longest chain in the product lattice: take the longest chains of `A` and
+`B`, and start with the product of their lowest elements. Then, increase
+the elements one at a time according to the chains. The simplest way to do
+that might be to increase by all elements of the `A` chain, and then
+by all of the elements of the `B` chain (or the other way around). That's the
+strategy I took when [constructing the \(\text{Sign} \times \text{Sign}\)
+chain above](#sign-prod-chain).
+
+To formalize this notion, a few lemmas. First, given two chains where
+one starts with the same element another ends with, we can combine them into
+one long chain.
+
+{{< codelines "agda" "agda-spa/Chain.agda" 31 33 >}}
+
+More interestingly, given a chain of comparisons in one lattice, we are
+able to lift it into a chain in another lattice by applying a function
+to each element. This function must be monotonic, because it must not
+be able to reverse \(a < b\) such that \(f(b) < f(a)\). Moreover, this function
+should be injective, because if \(f(a) = f(b)\), then a chain \(a < b\) might
+be collapsed into \(f(a) \not< f(a)\), changing its length. Finally,
+the function needs to produce equivalent outputs when giving equivalent inputs.
+The result is the following lemma:
+
+{{< codelines "agda" "agda-spa/Lattice.agda" 196 217 >}}
+
+Given this, and two lattices of finite height, we construct the full product
+chain by lifting the `A` chain into the product via \(a \mapsto (a, \bot)\),
+lifting the `B` chain into the product via \(b \mapsto (\top, b)\), and
+concatenating the results. This works because the first chain ends with
+\((\top, \bot)\), and the second starts with it.
+
+{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 177 179 >}}
+
+This gets us the longest chain; what remains is to prove that this chain's
+length is the bound of all other changes. To do so, we need to work in
+the opposite direction; given a chain in the product lattice, we need to
+somehow reduce it to chains in lattices `A` and `B`, and leverage their
+finite height to complete the proof.
+
+The key idea is that for every two consecutive elements in the product lattice
+chain, we know that at least one of their components must've increased.
+This increase had to come either from elements in lattice `A` or in lattice `B`.
+We can thus stick this increase into an `A`-chain or a `B`-chain, increasing
+its length. Since one of the chains grows with every consecutive pair, the
+number of consecutive pairs can't exceed the length of the `A` and `B` chains.
+
+I implement this idea as an `unzip` function, which takes a product chain
+and produces two chains made from its increases. By the logic we've described,
+the length two chains has to bound the main one's. I give the signature below,
+and will put the implementation in a collapsible detail block. One last
+detail is that the need to decide which chain to grow --- and thus which element
+has increased --- is what introduces the need for decidable equality.
+
+{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 158 >}}
+
+{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 172 "" "**(Click here for the implementation of `unzip`)**" >}}
+
+Having decomposed the product chain into constituent chains, we simply combine
+the facts that they have to be bounded by the height of the `A` and `B` lattices,
+as well as the fact that they bound the combined chain.
+
+{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 174 183 "hl_lines = 8-9" >}}
+
+This completes the proof!
+
 {{< todo >}}
 The rest of this.
 {{< /todo >}}