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
+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