diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md
index 22aa140..bb9a987 100644
--- a/content/blog/03_spa_agda_fixed_height.md
+++ b/content/blog/03_spa_agda_fixed_height.md
@@ -192,7 +192,7 @@ three or more comparisons.
 Thus, the above-below lattice has a length of two comparisons (or alternatively,
 three elements).
 
-{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}}
+{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 363 >}}
 
 And that's it.
 
@@ -300,7 +300,7 @@ 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" 165 175 "hl_lines = 8-9" >}}
+{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 165 175 "hl_lines = 8-10" >}}
 
 This completes the proof!
 
@@ -476,7 +476,7 @@ conversion functions, in both directions:
 
 With that, we can prove the second lattice's finite height:
 
-{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 73 >}}
+{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 80 >}}
 
 
 The conversion functions are also not too difficult to define. I give