 Here \(P\) is a variable of type \(\{0, \ldots ,i\} \rightarrow[e]^{i+1} \rightarrow [e]^j \rightarrow t\), while \(c\) is a variable of type [\(e]^i\) representing the input context of length \(i\), and \(c'\) is a variable of type [\(e]^j\) representing the output context. Note that the type \(\{0, \ldots ,i\} \rightarrow [e]^{i+1} \rightarrow [e]^j \rightarrow t\) for \(P\) indicates that \(P\) first takes an index in the range \(\{0, \ldots ,i\}\), next a context fitting this range (a context of length \(i+1)\), next a context of a yet unknown length, and then gives a truth value. \(P\) is the type of unary predicates, lifted to the level of context changers, as follows. Instead of using a variable to range over objects to form an expression of type \(e\), a lifted predicate uses a variable ranging over the size of an input context to form an expression that denotes a changer for that context. 