diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md
index fd28033..655ee83 100644
--- a/content/blog/01_spa_agda_lattices.md
+++ b/content/blog/01_spa_agda_lattices.md
@@ -242,6 +242,7 @@ record IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
         ⊔-idemp : (x : A) → (x ⊔ x) ≡ x
 ```
 
+Note that this is an example of the ["Is Something" pattern]({{< relref "agda_is_pattern" >}}).
 It turns out to be convenient, however, to not require definitional equality
 (`≡`). For instance, we might model sets as lists. Definitional equality
 would force us to consider lists with the same elements but a different
@@ -260,7 +261,7 @@ As it turns out, the `min` function has very similar properties to `max`:
 it's idempotent, commutative, and associative. For a partial order like
 ours, the analog to `min` is "greatest lower bound", or "the largest value
 that's smaller than both inputs". Such a function is denoted as \\(a\\sqcap b\\).
-Intuitively, where \\(s_1 \\sqcup s_2\\) means "combine two signs where
+As for what it means, where \\(s_1 \\sqcup s_2\\) means "combine two signs where
 you don't know which one will be used" (like in an `if`/`else`), 
 \\(s_1 \\sqcap s_2\\) means "combine two signs where you know both of
 them to be true". For example, \\((+\ \\sqcap\ ?)\ =\ +\\), because a variable
@@ -321,4 +322,19 @@ In Agda, we can therefore write a lattice as follows:
 
 {{< codelines "Agda" "agda-spa/Lattice.agda" 153 163 >}}
 
-### Concrete Example: 
+### Concrete Example: Natural Numbers
+
+Since we've been talking about `min` and `max` as motivators for properties
+of \\((\\sqcap)\\) and \\((\\sqcup)\\), it might not be all that surprising
+that natural numbers form a lattice with `min` and `max` as the two binary
+operations. In fact, the Agda standard library writes `min` as `_⊓_` and
+`max` as `_⊔_`! We can make use of the already-proven properties of these
+operators to easily define `IsLattice` for natural numbers. Notice that
+since we're not doing anything clever, like considering lists up to reordering,
+there's no reason not to use definitional equality `≡` for our equivalence relation.
+
+{{< codelines "Agda" "agda-spa/Lattice/Nat.agda" 1 45 >}}
+
+The definition for the lattice instance itself is pretty similar; I'll omit
+it here to avoid taking up a lot of vertical space, but you can find it
+on lines 47 through 83 of [my `Lattice.Nat` module]({{< codeurl "agda-spa/Lattice/Nat.agda" >}}).