5.4 Recoding

Definition 5.22

Let \( \gamma {\lt} \beta \) be proper type indices at most \( \alpha \). An object \( x : \mathsf{TSet}_\beta \) is called a \( \gamma \)-combination of a set of \( \beta \)-coding functions \( s \) with respect to a \( \beta \)-support \( S \) if

\[ U_\beta (x)(\gamma ) = \bigcup _{(V, v) \in \chi \in s,\, V \geq S} U_\beta (v)(\gamma ) \]

By extensionality, a set of coding functions \( s \) has at most one \( \gamma \)-combination with respect to a given support \( S \).

Proposition 5.23

If \( x \) is a \( \gamma \)-combination of \( s \) with respect to \( S \) then \( \rho (x) \) is a \( \gamma \)-combination of \( s \) with respect to \( \rho (S) \).

Proof ▶

We can calculate

\begin{align*} U_\beta (\rho (x))(\gamma ) & = \rho _\gamma [U_\beta (x)(\gamma )] \\ & = \rho _\gamma \left[ \bigcup _{(V, v) \in \chi \in s,\, V \geq S} U_\beta (v)(\gamma ) \right] \\ & = \bigcup _{(V, v) \in \chi \in s,\, V \geq S} \rho _\gamma \left[ U_\beta (v)(\gamma ) \right] \\ & = \bigcup _{(V, v) \in \chi \in s,\, V \geq S} U_\beta (\rho (v))(\gamma ) \\ & = \bigcup _{(V, v) \in \chi \in s,\, V \geq \rho (S)} U_\beta (v)(\gamma ) \end{align*}

where the last inequality uses the fact that coding functions are defined on a support orbit.

Definition 5.24

Let \( s \) be a set of \( \beta \)-coding functions, and let \( o \) be a \( \beta \)-support orbit such that for each \( S \in o \), \( s \) has a \( \gamma \)-combination \( x \) with respect to \( S \) where \( S \) supports \( x \). Then the \( (\gamma ,\beta ) \)-raised coding function for \( (s, o) \) is the relation \( \chi : \mathsf{StrSupp}_\beta \to \mathsf{TSet}_\beta \to \mathsf{Prop}\) defined by the constructor

\[ \forall S \in o,\, \forall x \text{ combinations of } (s, S),\, (S, x) \in \chi \]

Proposition 5.25

The \( (\gamma ,\beta ) \)-raised coding function for \( (s, o) \) is a coding function.

Proof ▶

Coinjectivity follows from uniqueness of combinations. The nonemptiness and support orbit conditions follow from the definition, as does the condition that \( (S, x) \in \chi \) implies that \( S \) is a support for \( x \). It remains to show that if \( (S, x) \in \chi \) and \( \rho \) is \( \beta \)-allowable, then \( (\rho (S), \rho (x)) \in \chi \), and this follows directly from proposition 5.23.

Definition 5.26 designated support

For a type index \( \beta \leq \alpha \), a \( \beta \)-set orbit is the quotient of \( \mathsf{TSet}_\beta \) under the relation of being in the same orbit under \( \beta \)-allowable permutations. We write \( [x] \) for the set orbit of \( x \). For each set orbit \( o \), we choose a representative \( \operatorname {\mathsf{repr}}(o) : \mathsf{TSet}_\beta \) with \( [\operatorname {\mathsf{repr}}(o)] = o \), and define a support \( S_o \) for \( \operatorname {\mathsf{repr}}(o) \). For each set, we choose a \( \beta \)-allowable permutation \( \operatorname {\mathsf{twist}}_t \) with the property that \( \operatorname {\mathsf{twist}}_t(\operatorname {\mathsf{repr}}([t])) = t \), and we define the designated support of \( t \) to be \( \operatorname {\mathsf{dsupp}}(t) = \operatorname {\mathsf{twist}}_t(S_{[t]}) \). This is a support for \( t \).

Definition 5.27

Let \( \gamma {\lt} \beta \) be proper type indices. Let \( S \) be a \( \beta \)-support and let \( u : \mathsf{TSet}_\gamma \). Then the \( (\gamma ,\beta ) \)-raised singleton coding function is

\[ \operatorname {\mathsf{raise}}(S, u) = \chi _{(\operatorname {\mathsf{singleton}}_\beta (u), S + \operatorname {\mathsf{dsupp}}(u)^\beta )} \]

A coding function is called a \( (\gamma ,\beta ) \)-raised singleton if it is of the form \( \operatorname {\mathsf{raise}}(S, u) \).

Proposition 5.28

Let \( \gamma {\lt} \beta \) be proper type indices, and let \( x : \mathsf{TSet}_\beta \). Then for any support \( S \) of \( x \), \( x \) is a combination of the set

\[ \{ \operatorname {\mathsf{raise}}(S, u) \mid u \in U_\beta (x)(\gamma ) \} \]

Proof ▶

We must show that

\[ U_\beta (x)(\gamma ) = \bigcup _{u \in U_\beta (x)(\gamma ),\, (V,v) \in \operatorname {\mathsf{raise}}(S, u),\, V \geq S} U_\beta (v)(\gamma ) \]

First, suppose \( u \in U_\beta (x)(\gamma ) \). Then we have

\[ (S + \operatorname {\mathsf{dsupp}}(u)^\beta , \operatorname {\mathsf{singleton}}_\beta (u)) \in \operatorname {\mathsf{raise}}(S, u);\quad u \in U_\beta (\operatorname {\mathsf{singleton}}_\beta (u))(\gamma ) \]

so the left-hand side is contained in the right-hand side.

For the converse, suppose that \( u \in U_\beta (x)(\gamma ) \) and \( (V, v) \in \operatorname {\mathsf{raise}}(S, u) \) with \( V \geq S \). As \( (V, v) \in \operatorname {\mathsf{raise}}(S, u) \), there is some \( \beta \)-allowable \( \rho \) such that

\[ \rho (S + \operatorname {\mathsf{dsupp}}(u)^\beta ) = V;\quad \rho (\operatorname {\mathsf{singleton}}_\beta (u)) = v \]

As \( V \geq S \), we obtain \( \rho (S) = S \), ¹ so \( \rho (x) = x \). Then

\begin{align*} U_\beta (v)(\gamma ) & = U_\beta (\rho (\operatorname {\mathsf{singleton}}_\beta (u)))(\gamma ) \\ & = U_\beta (\operatorname {\mathsf{singleton}}_\beta (\rho _\gamma (u)))(\gamma ) \\ & = \{ \rho _\gamma (u) \} \\ & \subseteq U_\beta (\rho (x))(\gamma ) \\ & = U_\beta (x)(\gamma ) \end{align*}

as required.

Proposition 5.29

Let \( \gamma {\lt} \beta \) be proper type indices, and let \( \chi \) be a \( \beta \)-coding function. Then there is a set of \( (\gamma ,\beta ) \)-raised singletons \( s \) and support orbit \( o \) such that \( \chi \) is the \( (\gamma ,\beta ) \)-raised coding function for \( (s, o) \).

Proof ▶

Let \( \chi \) be a \( \beta \)-coding function, and let \( (S, x) \in \chi \). Let

\[ s = \{ \operatorname {\mathsf{raise}}(S, u) \mid u \in U_\beta (x)(\gamma ) \} \]

Let \( o \) be the support orbit such that \( T \in o \) if and only if \( T \in \operatorname {\mathsf{coim}}\chi \). We claim that \( \chi \) is the raised coding function for \( (s, o) \). It suffices to show that \( (S, x) \) is in this raised coding function. That is, we must show that \( S \in o \), which is trivial, and that \( x \) is a combination of \( s \), which is the content of proposition 5.28.