-boxed types. Here, a "boxed type" is a type function with one missing
-piece, which we can think of as a function from a type to a type.
-Call this type function M, and let P, Q, R, and S be variables over types.
-
-Recall that a monad requires a singleton function 1:P-> MP, and a
-composition operator >=>: (P->MQ) -> (Q->MR) -> (P->MR) [the type for
-the composition operator given here corrects a "type"-o from the class handout]
-that obey the following laws:
-
- 1 >=> k = k
- k >=> 1 = k
- j >=> (k >=> l) = (j >=> k) >=> l
-
-For instance, the identity monad has the identity function I for 1
-and ordinary function composition (o) for >=>. It is easy to prove
-that the laws hold for any expressions j, k, and l whose types are
-suitable for 1 and >=>:
-
- 1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k
- k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k
-
- (j >=> k) >=> l == (\p.j(kp)) o l == \q.(\p.j(kp))(lq) ~~> \q.j(k(lq))
- j >=> (k >=> l) == j o (k o l) == j o \p.k(lp) == \q.j(\p.k(lp)q) ~~> \q.j(k(lq))
-
-1. On a number of occasions, we've used the Option type to make our
-conceptual world neat and tidy (for instance, think of the discussion
-of Kaplan's Plexy). As we learned in class, there is a natural monad
-for the Option type. Borrowing the notation of OCaml, let's say that
-"`'a option`" is the type of a boxed `'a`, whatever type `'a` is.
+boxed types. Here, a "boxed type" is a type function with one unsaturated
+hole (which may have several occurrences, as in `(α,α) tree`). We can think of the box type
+as a function from a type to a type.
+
+Recall that a monad requires a singleton function <code>⇧ (\* mid \*) : P-> <u>P</u></code>, and a
+composition operator like <code>>=> : (P-><u>Q</u>) -> (Q-><u>R</u>) -> (P-><u>R</u>)</code>.
+
+As we said in the notes, we'll move freely back and forth between using `>=>` and using `<=<` (aka `mcomp`), which
+is just `>=>` with its arguments flipped. `<=<` has the virtue that it corresponds more
+closely to the ordinary mathematical symbol `○`. But `>=>` has the virtue
+that its types flow more naturally from left to right.
+
+Anyway, `mid`/`⇧` and (let's say) `<=<` have to obey the Monad Laws:
+
+ ⇧ <=< k == k
+ k <=< ⇧ == k
+ j <=< (k <=< l) == (j <=< k) <=< l
+
+For example, the Identity monad has the identity function `I` for `⇧`
+and ordinary function composition `○` for `<=<`. It is easy to prove
+that the laws hold for any terms `j`, `k`, and `l` whose types are
+suitable for `⇧` and `<=<`:
+
+ ⇧ <=< k == I ○ k == \p. I (k p) ~~> \p. k p ~~> k
+ k <=< ⇧ == k ○ I == \p. k (I p) ~~> \p. k p ~~> k
+
+ (j <=< k) <=< l == (\p. j (k p)) ○ l == \q. (\p. j (k p)) (l q) ~~> \q. j (k (l q))
+ j <=< (k <=< l) == j ○ (k ○ l) == j ○ (\p. k (l p)) == \q. j ((\p. k (l p)) q) ~~> \q. j (k (l q))
+
+1. On a number of occasions, we've used the Option/Maybe type to make our
+conceptual world neat and tidy (for instance, think of [[our discussion
+of Kaplan's Plexy|topics/week6_plexy]]). As we learned in class, there is a natural monad
+for the Option type. Using the vocabulary of OCaml, let's say that
+`'a option` is the type of a boxed `'a`, whatever type `'a` is.