In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
-Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where if `α list` is our box type, we can write the second type as:
+Note that either of the schemas `P` or `Q` are permitted to themselves be boxed
+types. That is, if `α list` is our box type, we can write the second type as:
<code><u>int</u> -> <u>int list</u></code>
+And also what the rhs there is a boxing of is itself a boxed type (with the same kind of box):, so we can write it as:
+
+<code><u>int</u> -> <span class="box2">int</span></code>
+
+We have to be careful though not to to unthinkingly equivocate between different kinds of boxes.
+
Here are some examples of values of these Kleisli arrow types, where the box type is `α list`, and the Kleisli arrow types are <code>int -> <u>int</u></code> (that is, `int -> int list`) or <code>int -> <u>bool</u></code>:
<pre>\x. [x]