Dependencies

The cloud relation \( \prec \) on codes is given by the constructor

where \( \beta , \gamma {\lt} \alpha \) are distinct and \( \gamma \) is proper.

A code is a pair \( c = (\beta , s) \) where \( \beta {\lt} \alpha \) is a type index and \( s \) is a nonempty set of \( \mathsf{TSet}_\beta \).

We define the relation \( \looparrowright \) between codes by the following two constructors.

• If \( c \) is a \( \prec \)-even code, then \( c \looparrowright c \).

• If \( c \) is a \( \prec \)-even code and \( c \prec d \), then \( c \looparrowright d \).

This relation is cofunctional (definition A.1): if \( d \) is a code, there is exactly one \( c \) such that \( c \looparrowright d \). Moreover, if \( c \looparrowright (\beta , s_1), (\beta , s_2) \), then \( s_1 = s_2 \).

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.

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

We define a function \( \operatorname {\mathsf{singleton}}_\alpha \) for each lower type index \( \beta \) from \( \mathsf{TSet}_\beta \) to the type of new t-sets by \( x \mapsto (\beta , \{ x\} ) \). The given code is even as all singleton codes are even. This satisfies \( U_\alpha (\operatorname {\mathsf{singleton}}_\alpha (x))(\beta ) = \{ x \} \).

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.

We define a function \( \operatorname {\mathsf{typed}}_\alpha \) from the type of near-litters to the type of new t-sets by mapping a near-litter \( N \) to the code \( (\bot , N) \). This code is even as all codes of the form \( (\bot , s) \) are even. This function is clearly injective, and satisfies

by definition.

Define an action of allowable permutations on codes by

Then

1. \( c \prec d \) implies \( \rho (c) \prec \rho (d) \);

2. \( c \looparrowright d \) implies \( \rho (c) \looparrowright \rho (d) \);

3. \( c \) is even if and only if \( \rho (c) \) is even;

4. \( x \in _\beta c \) if and only if \( \rho (\beta )(x) \in _\beta \rho (c) \).

The cloud relation is injective (definition A.1). That is, if \( c_1, c_2 \prec d \), then \( c_1 = c_2 \).

The cloud relation is well-founded.

Let \( x : \mathsf{TSet}_\beta \) for some type index \( \beta {\lt} \alpha \), and let \( c \) be a code. We say that \( x \) is a type-\( \beta \) member of \( c \) if there is a set \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\beta \) such that \( x \in s \) and \( c \looparrowright (\beta , s) \), and hence for all sets \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\beta \) such that \( c \looparrowright (\beta , s) \), we have \( x \in s \) by definition 3.7. We write \( x \in _\beta c \). Note that this definition is only useful when \( c \) is even.

Let \( c_1, c_2 \) be even codes. If \( \beta {\lt} \alpha \) is a proper type index such that

then \( c_1 = c_2 \).

If \( c \prec (\gamma , s_1) \) and \( c \prec (\gamma , s_2) \), then \( s_1 = s_2 \).

Using the model data from definition 3.12, if \( \# \mathsf{Tang}_\alpha \leq \# \mu \), then there is a position function on the type of \( \alpha \)-tangles, ¹ such that

• if \( N \) is a near-litter and \( t \) is an \( \alpha \)-tangle such that \( \operatorname {\mathsf{set}}(t) = \operatorname {\mathsf{typed}}_\alpha (N) \), we have \( \iota (N) \leq \iota (t) \); and

• if \( t \) is an \( \alpha \)-tangle and \( x \) is an atom or near-litter that occurs in the range of \( \operatorname {\mathsf{supp}}(t)_A \), then \( \iota (x) {\lt} \iota (t) \).

Let \( \prec \) be a relation on a type \( \tau \). We say that an object \( x : \tau \) is \( \prec \)-even if all of its \( \prec \)-predecessors are odd; we say that \( x \) is \( \prec \)-odd if it has a \( \prec \)-predecessor that is even. Then:

1. Minimal objects are even.

2. If \( \prec \) is well-founded, then every object \( x : \tau \) is either even or odd, but not both.