type variable. So if our box type is `α List`, and `α == Int`, we
would write
-<table border=2px><td>Int</td></table>
+<u>Int</u>
for the type of a boxed Int.
At the most general level, we'll talk about *Kleisli arrows*:
-P -> <table border=2px><td>Q</td></table>
+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 -> <table border=2px><td>Bool</td></table>
+Int -> <u>Bool</u>
-Int List -> <table border=2px><td>Int List</td></table>
+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
-<table border=2px><td>Int</td></table>
-->
-<table border=2px><td><table
-border=2px><td>Int</td></table></td></table>
-
+<u>Int</u> -> <u><u>Int</u></u>