+for the type of a boxed Int.
+
+At the most general level, we'll talk about *Kleisli arrows*:
+
+P -> <u>Q</u>
+
+A Kleisli arrow is the type of a function from objects of type P to
+objects of type box Q, for some choice of type expressions P and Q.
+For instance, the following are arrows:
+
+Int -> <u>Bool</u>
+
+Int List -> <u>Int List</u>
+
+Note that the left-hand schema can itself be a boxed type. That is,
+if `α List` is our box type, we can write the second arrow as
+
+<u>Int</u> -> <u><u>Int</u></u>