Continue expanding on the map draft

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

content/blog/02_spa_agda_combining_lattices.md

@@ -151,9 +151,10 @@ Let's start thinking about what sorts of lattices our maps will be.
 The thing that [motivated our introduction]({{< relref "01_spa_agda_lattices#specificity" >}})
 of lattices was comparing them by "specificity", so let's try figure out how
 to compare maps. For that, we can begin small, by looking at singleton maps.
-If we have `{"x": +}` and `{"x": ⊤}`, which one of them is smaller? Well, wehave previously established that `+` is more specific (and thus less than) `⊤`. Thus, it shouldn't be too much of a stretch
+If we have `{"x": +}` and `{"x": ⊤}`, which one of them is smaller? Well, we have
-to say that for singleton maps of the same key, the one with the smaller
+previously established that `+` is more specific (and thus less than) `⊤`. Thus,
-value is smaller.
+it shouldn't be too much of a stretch to say that for singleton maps of the same
+key, the one with the smaller value is smaller.
 
 Now, what about a pair of singleton maps like `{"x": +}` and `{"y": ⊤}`? Among
 these two, each contains some information that the other does not. Although the
@@ -163,4 +164,56 @@ these maps incompatible, then. More generally, if we have two maps and each one
 has a key that the other doesn't, we can't compare them.
 
 If only one map has a unique key, though, things are different. Take for
-instance `{"x": +}` and `{"x": +, "y": +}`.
+instance `{"x": +}` and `{"x": +, "y": +}`. Are they really incomparable?
+The keys that the two maps do share can be compared (`+ <= +`, because they're
+equal).
+
+
+All of the above leads to the following conventional definition, which I find
+easier to further motivate using \((\sqcup)\) and \((\sqcap)\)
+(and [do so below]({{< relref "#union-as-or" >}})).
+
+> A map `m1` is less than or equal to another map `m2` (`m1 <= m2`) if for
+> every key `k` that has a value in `m1`, the key also has a value in `m2`, and
+> `m1[k] <= m2[k]`.
+
+That definitions matches our intuitions so far. The only key in `{"x": +}` is `x`;
+this key is also in `{"x": ⊤}` (check) and `+ < ⊤` (check). On the other hand,
+both `{"x": +}` and `{"y": ⊤}` have a key that the other doesn't, so the
+definition above is not satisfied. Finally, for `{"x": +}` and
+`{"x": +, "y": +}`, the only key in the former is also present in the latter,
+and `+ <= +`; the definition is satisfied.
+
+Next, we need to define the \((\sqcup)\) and \((\sqcap)\) operators that match
+our definition of "less than or equal". Let's start with \((\sqcup)\). For two
+maps \(m_1\) and \(m_2\), the join of those two maps, \(m_1 \sqcup m_2\) should
+be greater than or equal to both; in other words, both sub-maps should be less
+than or equal to the join. Our newly-introduced condition for "less than or equal"
+requires that each key in the smaller map be present in the larger one; as
+a result, \(m_1 \sqcup m_2\) should contain all the keys in \(m_1\) __and__
+all the keys in \(m_2\). So, we could just take the union of the two maps:
+copy values from both into the result. Only, what happens if both \(m_1\)
+and \(m_2\) have a value mapped to a particular key? The values in the two
+maps could be distinct, and they might even be incomparable. This is where the
+second part of the condition kicks in: the value in the combination of the
+maps needs to be bigger than the value in either sub-map. We already know how
+to get a value that's bigger than two other values: we use a join on the
+values! Thus, define \(m_1 \sqcup m_2\) as a map that has all the keys
+from \(m_1\) and \(m_2\), where the value at a particular key is given
+as follows:
+
+{{< latex >}}
+(m_1 \sqcup m_2)[k] =
+\begin{cases}
+m_1[k] \sqcup m_2[k] & k \in m_1, k \in m_2 \\
+m_1[k] & k \in m_1, k \notin m_2 \\
+m_2[k] & k \notin m_1, k \in m_2
+\end{cases}
+{{< /latex >}}
+
+{{< todo >}}
+I started using 'join' but haven't introduced it before.
+{{< /todo >}}
+
+something something lub glub
+{#union-as-or}