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, if `α list` is our box type, and `P` is to boxed type
+type. That is, if `α list` is our box type, and `P` is the boxed type
`int list`, we can write the boxed type that has `P` as its left-hand
side as
If it's clear that we're uniformly talking about the same box type (in
this example, `α list`), we can equivalently write
-<code><u>int</u> -> <u><u>int</u></u></code>
+<code><u>int</u> -> <span class="box2">int</span></code>
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>: