ame and obsessing over wording: name a more iconic duo

you can't.

Author: plt-amy

src/1Lab/intro.lagda.md

@@ -1327,13 +1327,11 @@ However, an inhabitant of this type has a much more interesting
 _topological_ interpretation!
 
 <details open>
-<summary>**Worked example**: Interpreting dependent sums as fibrations and
-dependent products as sections lets us derive topological
-interpretations for types.
-
-We show how to do this for the type $(x\ y : A) \to x \equiv y$, and
-show that a space $A$ admitting an inhabitant of this type has the
-property of being "contractible if inhabited".
+<summary>**Worked example**: Interpreting dependent sums as fibrations
+and dependent products as sections lets us derive topological
+interpretations for types. We show how to do this for the type $(x\ y :
+A) \to x \equiv y$, and show that a space $A$ admitting an inhabitant of
+this type has the property of "being contractible if it is inhabited".
 </summary>
 
 First, we'll shuffle the type so that we can phrase it in terms of a
@@ -1359,11 +1357,12 @@ endpoints of a path --- so we will write it $(d_0,d_1) : A^\bb{I}
 \to A \times A$, since it is the pairing of the maps which evaluate a
 path at the left and right endpoints of the interval.
 
-As a very quick aside, there is a map $r : \lambda x.\ (x, x,
-\id{refl})$, we get a diagram like the one below, expressing that
-the diagonal $A \to A \times A$ can be factored as a weak equivalence
-follwed by a fibration, exhibiting $A^\bb{I}$ as a path space object
-for $A$.
+As a very quick aside, there is a map $r : \lambda x.\ (x, x, \id{refl}$
+making the diagram below commute. This diagram expresses that the
+diagonal $A \to A \times A$ can be factored as a weak equivalence
+follwed by a fibration through $A^\bb{I}$, which is the defining
+property of a _path space object_.
+$A$.
 
 $$
 A \xrightarrow{\~r} A^\bb{I} \xrightarrow{(d0,d1)} \to A \times A

src/Cat/Functor/Monadic/Beck.lagda.md

@@ -61,13 +61,14 @@ Suppose that we are given a $T$-algebra $(A, \nu)$. Note that $(TA,
 $A$. Let us illustrate this with a concrete example: Suppose we have the
 cyclic group $\bb{Z}/n\bb{Z}$, for some natural number $n$, which we
 regard as a subgroup of $\bb{Z}$. The corresponding algebra $(TA, \mu)$
-would be the [free group] on one generator --- the group of integers
----, whence we conclude that, in general, this $(TA, \mu)$ algebra
+would be the [free group] on one generator^[the group of integers]
+whence^[I was feeling pretentious when I wrote this sentence] we
+conclude that, in general, this "free-on-underlying" $(TA, \mu)$ algebra
 is very far from being the $(A, \nu)$ algebra we started with.
 
 [free group]: Algebra.Group.Free.html
 
-Still thinking about our $\bb{Z}/n\bb{Z}$ example, it feels like we
+Still, motivated by our $\bb{Z}/n\bb{Z}$ example, it feels like we
 should be able to [quotient] the algebra $(TA, \mu)$ by some set of
 _relations_ and get back the algebra $(A, \nu)$ we started with. This is
 absolutely true, and it's true even when the category of $T$-algebras is
@@ -79,17 +80,21 @@ lacking in quotients! In particular, we have the following theorem:
 
 [coequaliser]: Cat.Diagram.Coequaliser.html
 
-~~~{.quiver .short-1}
+~~~{.quiver .short-15}
 \[\begin{tikzcd}
-  {(T^2A,\mu)} & {(TA,\mu)} & {(A,\nu)}
+  {T^2A} & {TA} & {A,}
   \arrow["\mu", shift left=1, from=1-1, to=1-2]
   \arrow["T\nu"', shift right=1, from=1-1, to=1-2]
-  \arrow[from=1-2, to=1-3]
+  \arrow["\nu", from=1-2, to=1-3]
 \end{tikzcd}\]
 ~~~
 
-Furthermore, the arrows $\mu$ and $T\nu$ have a common left inverse, so
-this is a reflexive coequaliser, called the **Beck coequaliser**.
+called the **Beck coequaliser** (of $A$). Furthermore, this coequaliser
+is _reflexive_ in $\ca{C}^T$, meaning that the arrows $\mu$ and $T\nu$
+have a common right inverse. Elaborating a bit, this theorem lets us
+decompose any $T$-algebra $(A, \nu)$ into a canonical presentation of
+$A$ by generators and relations, as a quotient of a free algebra by a
+relation (induced by) the fold $\nu$.
 
 <!--
 ```agda
@@ -116,9 +121,12 @@ module _ (Aalg : Algebra C T) where
 ```
 -->
 
-The calculation is just.. well, calculation, so we present it without
-much further commentary. Observe that $\nu$ coequalises $\mu$ and $T\nu$
-essentially by the definition of being an algebra map.
+**Proof**. The proof is by calculation, applying the monad laws where
+applicable, so we present it without much further commentary. Observe
+that $\nu$ coequalises $\mu$ and $T\nu$ essentially by the definition of
+being an algebra map. Note that we do not make use of the fact that the
+monad $T$ was given by a _specified_ adjunction $F \dashv U$ in the
+proof, and any adjunction presenting $T$ will do.
 
 ```agda
   open is-coequaliser