content/blog/01_spa_agda_lattices.md

@@ -202,7 +202,6 @@ similar function for our signs. We call this function "[least upper bound](https
 since it is the "least (most specific)
 element that's greater (less specific) than either `s1` or `s2`". Conventionally,
 this function is written as \(a \sqcup b\) (or in our case, \(s_1 \sqcup s_2\)).
-The \((\sqcup)\) symbol is also called the _join_ of \(a\) and \(b\).
 We can define it for our signs so far using the following [Cayley table](https://en.wikipedia.org/wiki/Cayley_table).
 
 {{< latex >}}
@@ -265,8 +264,7 @@ and the "least upper bound" function can be constructed from one another.
 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\),
+that's smaller than both inputs". Such a function is denoted as \(a\sqcap b\).
-and often called the "meet" of \(a\) and \(b\).
 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

content/blog/02_spa_agda_combining_lattices.md

@@ -449,6 +449,10 @@ The same is true for maps, under certain conditions.
 The finite-height property is crucial to lattice-based static program analysis;
 we'll talk about it in more detail in the next post of this series.
 
+{{< todo >}}
+I started using 'join' but haven't introduced it before.
+{{< /todo >}}
+
 ### Appendix: Proof of Uniqueness of Keys
 
 I will provide sketches of the proofs here, and omit the implementations

themes/vanilla

@@ -1 +1 @@
-Subproject commit 25e9057dd8b1ddc571f3b26d80b72e86bbcbaa72
+Subproject commit a4bff7623dc7c4b05b59714d7b919857a876422c