3.2 Model data defined
A new allowable permutation is a dependent function \( \rho \) of type \( \prod _{\beta {\lt} \alpha } \mathsf{AllPerm}_\beta \), subject to the condition
for every \( t : \mathsf{Tang}_\beta \). These form a group and have a \( \texttt{StrPermClass}_\alpha \) instance.
Define an action of allowable permutations on codes by
Then
\( c \prec d \) implies \( \rho (c) \prec \rho (d) \);
\( c \looparrowright d \) implies \( \rho (c) \looparrowright \rho (d) \);
\( c \) is even if and only if \( \rho (c) \) is even;
\( x \in _\beta c \) if and only if \( \rho (\beta )(x) \in _\beta \rho (c) \).
Part 1. Suppose that \( c \prec d \). Then, writing \( c = (\beta , s) \) and \( d = (\gamma , s') \), we obtain
Now, note that
So \( \rho (c) \prec \rho (d) \) as required.
Part 2. Direct.
Part 3. Follows from the general fact that if \( f : \tau \to \sigma \) is a bijection and we have \( x \prec _\tau y \) if and only if \( f(x) \prec _\sigma f(y) \), then the \( \prec _\tau \)-parity of \( x \) is the same as the \( \prec _\sigma \)-parity of \( f(x) \).
Part 4. We only need to show one direction, because we can apply the one-directional result to \( \rho ^{-1} \) to obtain the converse. Suppose that \( x \in _\beta c \), so \( c \looparrowright (\beta , s) \) and \( x \in s \). Then \( \rho (c) \looparrowright (\beta , \rho (\beta )[s]) \), so \( \rho (\beta )(x) \in _\beta \rho (c) \) as required,
A new t-set is an even code \( c \) such that there is an \( \alpha \)-support that supports \( c \) under the action of new allowable permutations, or a designated object called the empty set. New allowable permutations act on new t-sets in the same way that they act on codes, and map the empty set to itself. We define the map \( U_\alpha \) from new t-sets to \( \mathsf{StrSet}_\alpha \) by cases from the top of the path in the obvious way (using recursion on paths and the membership relation from proposition 3.8). It is easy to check that \( \rho (U_\alpha (x)) = U_\alpha (\rho (x)) \) by proposition 3.10.
Given model data, position functions, and typed near-litters for all types \( \beta {\lt} \alpha \), new model data is the model data at level \( \alpha \) consisting of new t-sets (definition 3.11) and new allowable permutations (definition 3.9). The embedding from new t-sets to \( \mathsf{StrSet}_\alpha \) is defined by