From ee8b1f5dc0a1d7271b1caa5da21026eda3a63d37 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Tue, 21 May 2024 19:04:08 -0700
Subject: [PATCH] Write a bit more, enable support for paragraph links

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 config.toml                                   |  4 ++
 content/blog/01_spa_agda_lattices.md          |  1 +
 .../blog/02_spa_agda_combining_lattices.md    | 44 +++++++++++++++++--
 3 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/config.toml b/config.toml
index 9a21344..a7635c3 100644
--- a/config.toml
+++ b/config.toml
@@ -33,6 +33,10 @@ defaultContentLanguage = 'en'
         [markup.goldmark.extensions.passthrough.delimiters]
           block = [['\[', '\]'], ['$$', '$$']]
           inline = [['\(', '\)']]
+    [markup.goldmark.parser]
+      [markup.goldmark.parser.attribute]
+        block = true
+        title = true
 
 [languages]
   [languages.en]
diff --git a/content/blog/01_spa_agda_lattices.md b/content/blog/01_spa_agda_lattices.md
index ee7f305..89dff36 100644
--- a/content/blog/01_spa_agda_lattices.md
+++ b/content/blog/01_spa_agda_lattices.md
@@ -249,6 +249,7 @@ It turns out to be convenient, however, to not require definitional equality
 would force us to consider lists with the same elements but a different
 order to be unequal. Instead, we parameterize our definition of `IsSemilattice`
 by a binary relation `_≈_`, which we ask to be an [equivalence relation](https://en.wikipedia.org/wiki/Equivalence_relation).
+{#definitional-equality}
 
 {{< codelines "Agda" "agda-spa/Lattice.agda" 23 39 >}}
 
diff --git a/content/blog/02_spa_agda_combining_lattices.md b/content/blog/02_spa_agda_combining_lattices.md
index 5a80506..af43f97 100644
--- a/content/blog/02_spa_agda_combining_lattices.md
+++ b/content/blog/02_spa_agda_combining_lattices.md
@@ -52,10 +52,13 @@ for both types:
 
 Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where
 \(l_1 \in L_1\) and \(l_2 \in L_2\). The first thing we can get out of the
-way is define what it means for two such elements to be equal. That's easy
-enough: we have an equality predicate `_≈₁_` that checks if an element
+way is define what it means for two such elements to be equal. Recall that
+we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitional-equality" >}})
+instead of definitional equality to allow similar elements to be considered
+equal; we'll have to define a similar relation for our new product lattice.
+That's easy enough: we have an equality predicate `_≈₁_` that checks if an element
 of \(L_1\) is equal to another, and we have `_≈₂_` that does the same for \(L_2\).
-It's reasonably to say that _pairs_ of elements are equal if their respective
+It's reasonable to say that _pairs_ of elements are equal if their respective
 first and second elements are equal:
 
 {{< latex >}}
@@ -65,3 +68,38 @@ first and second elements are equal:
 In Agda:
 
 {{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 39 40 >}}
+
+Verifying that this relation has the properties of an equivalence relation
+boils down to the fact that `_≈₁_` and `_≈₂_` are themselves equivalence
+relations.
+
+{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 42 48 >}}
+
+In fact, defining \((\sqcup)\) and \((\sqcap)\) by simply applying the
+corresponding operators from \(L_1\) and \(L_2\) seems quite natural as well.
+
+{{< latex >}}
+(l_1, l_2) \sqcup (j_1, j_2) \triangleq (l_1 \sqcup_1 j_1, l_2 \sqcup_2 j_2) \\
+(l_1, l_2) \sqcap (j_1, j_2) \triangleq (l_1 \sqcap_1 j_1, l_2 \sqcap_2 j_2)
+{{< /latex >}}
+
+In Agda:
+
+{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 50 54 >}}
+
+All that's left is to prove the various (semi)lattice properties. Intuitively,
+we can see that since the "combined" operator `_≈_` just independently applies
+the element operators `_≈₁_` and `_≈₂_`, as long as they are idempotent,
+commutative, and associative, so is the "combined" operator itself.
+Moreover, the proofs that `_⊔_` and `_⊓_` form semilattices are identical
+up to replacing \((\sqcup)\) with \((\sqcap)\). Thus, in Agda, we can write
+the code once, parameterizing it by the binary operators involved (and proofs
+that these operators obey the semilattice laws).
+
+{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 56 82 >}}
+
+Similarly to the semilattice properties, proving lattice properties boils
+down to applying the lattice properties of \(L_1\) and \(L_2\) to
+individual components.
+
+{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 84 96 >}}