Dependencies

Let \( t : \mathsf{Tang}_\beta \). Then we define the coding function \( \chi _t \) by the constructor

This is clearly a coding function, and satisfies \( (\operatorname {\mathsf{supp}}(t), \operatorname {\mathsf{set}}(t)) \in \chi _t \).

Let \( t, u : \mathsf{Tang}_\beta \). Then \( \chi _t = \chi _u \) if and only if there is a \( \beta \)-allowable \( \rho \) with \( \rho (t) = u \).

For any type index \( \beta \leq \alpha \), a \( \beta \)-coding function is a relation \( \chi : \mathsf{StrSupp}_\beta \to \mathsf{TSet}_\beta \to \mathsf{Prop}\) such that:

• \( \chi \) is coinjective;

• \( \chi \) is nonempty;

• if \( (S, x) \in \chi \), then \( S \) is a support for \( x \);

• if \( S, T \in \operatorname {\mathsf{coim}}\chi \) then \( S \) and \( T \) are in the same support orbit;

• if \( (S, x) \in \chi \) and \( \rho \) is \( \beta \)-allowable, then \( (\rho (S), \rho (x)) \in \chi \).

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

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

Let \( S, T \) be strong \( \beta \)-supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then for each \( A \), we define the base action \( \operatorname {\mathsf{conv}}_{S_A, T_A} \) to be \( (\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}, \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}) \); this is a base action by ??. We now define the \( \beta \)-action \( \operatorname {\mathsf{conv}}_{S,T} \) by \( (\operatorname {\mathsf{conv}}_{S,T})_A = \operatorname {\mathsf{conv}}_{S_A,T_A} \).

Let \( S \) and \( T \) be base supports. We define the relations \( \operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}, \operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}\) by the constructors ²

Note that \( {\operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}}^{-1} = \operatorname {\mathsf{conv}}_{T,S}^{\mathcal A}\) and \( {\operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}}^{-1} = \operatorname {\mathsf{conv}}_{T,S}^{\mathcal N}\).

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 \).

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

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

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

An atom condition is a pair \( (s, t) \) where \( s, t : \operatorname {\mathsf{Set}}\kappa \). A \( \beta \)-near-litter condition is either

• a flexible condition, consisting of a set \( s : \operatorname {\mathsf{Set}}\kappa \); or

• an inflexible condition, consisting of an inflexible \( \beta \)-path \( I = (\gamma ,\delta ,\varepsilon ,A) \), a \( \delta \)-coding function \( \chi \), and two \( \delta \)-trees \( R^{\mathcal A}, R^{\mathcal N}\) of relations on \( \kappa \).

A \( \beta \)-specification is a pair \( (\sigma ^{\mathcal A}, \sigma ^{\mathcal N}) \) where

• \( \sigma ^{\mathcal A}\) is a \( \beta \)-tree of enumerations of atom conditions; and

• \( \sigma ^{\mathcal N}\) is a \( \beta \)-tree of enumerations of \( \beta \)-near-litter conditions.

A \( \beta \)-support \( S \) is strong if:

• for every pair of near-litters \( N_1, N_2 \in \operatorname {\mathsf{im}}S_A^{\mathcal N}\), we have \( \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{im}}S_A^{\mathcal A}\); and

• for every inflexible path \( I = (\gamma ,\delta ,\varepsilon ,A) \) and \( t : \mathsf{Tang}_\delta \), if there is a near-litter \( N \in \operatorname {\mathsf{im}}S_{{A_\varepsilon }_\bot }^{\mathcal N}\) with \( N^\circ = f_{\delta ,\varepsilon }(t) \), then \( \operatorname {\mathsf{supp}}(t) \preceq S_{A_\delta } \).

We define a preorder \( \preceq \) on base supports by \( S \preceq T \) if and only if \( \operatorname {\mathsf{im}}S^{\mathcal A}\subseteq \operatorname {\mathsf{im}}T^{\mathcal A}\) and \( \operatorname {\mathsf{im}}S^{\mathcal N}\subseteq \operatorname {\mathsf{im}}T^{\mathcal N}\). For \( \beta \)-supports, we define \( S \preceq T \) if and only if \( S_A \preceq T_A \) for each \( A \).

Let \( S \) be a \( \beta \)-support. Then its specification is the \( \beta \)-specification \( \sigma = \operatorname {\mathsf{spec}}(S) \) given by the following constructors.

• Whenever \( (i, a) \in S_A^{\mathcal A}\), we have \( (i, (s, t)) \in \sigma _A^{\mathcal A}\) where

  \[ s = \{ j : \kappa \mid (j, a) \in S_A^{\mathcal A}\} ;\quad t = \{ j : \kappa \mid \exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a \in N \} \]

• Whenever \( (i, N) \in S_A^{\mathcal N}\) and \( N^\circ \) is \( A \)-flexible, we have \( (i, c) \in \sigma _A^{\mathcal N}\) where \( c \) is the flexible condition given by

  \[ s = \{ j : \kappa \mid \exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N^\circ = {N’}^\circ \} \]

• Whenever \( I = (\gamma ,\delta ,\varepsilon ,A) \) is an inflexible \( \beta \)-path, \( t : \mathsf{Tang}_\delta \), and \( (i, N) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) is such that \( N^\circ = f_{\delta ,\varepsilon }(t) \), we have \( (i, c) \in \sigma _{{A_\varepsilon }_\bot }^{\mathcal N}\) where \( c \) is the inflexible condition given by path \( I \) and coding function \( \chi _t \), and \( R^{\mathcal A}\) and \( R^{\mathcal N}\) are the \( \delta \)-trees of relations given by the constructors

  \begin{align*} & \forall i,\, \forall j,\, \forall a,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\to (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\to (i, j) \in R_B^{\mathcal A}\\ & \forall i,\, \forall j,\, \forall N,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\to (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}\to (i, j) \in R_B^{\mathcal N}\end{align*}

For a type index \( \beta \leq \alpha \), a \( \beta \)-support orbit is the quotient of \( \mathsf{StrSupp}_\beta \) under the relation of being in the same orbit under \( \beta \)-allowable permutations. ¹

A weak \( \beta \)-specification is a triple \( W = (R^{\mathcal A}, R^{\mathcal N}, \sigma ) \) where \( R^{\mathcal A}, R^{\mathcal N}\) are \( \beta \)-trees of relations on \( \kappa \), and \( \sigma \) is a \( \beta \)-specification. We say that a weak specification specifies a support \( S \) if there is a strong support \( T \) such that \( \sigma = \operatorname {\mathsf{spec}}(T) \), \( S \preceq T \), and

There are less than \( \# \mu \)-many \( \beta \)-coding functions for all type indices \( \beta \leq \alpha \).

There are less than \( \# \mu \) \( \bot \)-coding functions.

There are less than \( \# \mu \) \( \beta \)-coding functions if \( \beta \) is the minimal inhabitant of \( \lambda \).

Let \( \beta \) be a type index (which in practice will be \( \bot \) or the lowest proper type index). Suppose that there are less than \( \# \mu \) \( \beta \)-support orbits. Let \( \nu \) be a cardinal less than \( \# \mu \) such that for each \( \beta \)-support \( S \), there are at most \( \nu \)-many objects \( x : \mathsf{TSet}_\beta \) that \( S \) supports. Then there are less than \( \# \mu \) \( \beta \)-coding functions.

Suppose that for all type indices \( \delta {\lt} \beta \), there are strictly less than \( \# \mu \)-many \( \delta \)-coding functions. Then if \( \gamma {\lt} \beta \) is a proper type index, there are strictly less than \( \# \mu \) \( (\gamma ,\beta ) \)-raised singletons.

Suppose that for all type indices \( \delta {\lt} \beta \), there are strictly less than \( \# \mu \)-many \( \delta \)-coding functions. Then there are less than \( \# \mu \) \( \beta \)-specifications.

Suppose that for all type indices \( \delta {\lt} \beta \), there are strictly less than \( \# \mu \)-many \( \delta \)-coding functions. Then there are less than \( \# \mu \) \( \beta \)-support orbits.

Let \( S \) be a base support. Then \( S \) supports at most \( 2^{\# \kappa } \)-many sets \( s : \operatorname {\mathsf{Set}}{\mathcal A}\) under the action of base permutations.

For each type index \( \beta \leq \alpha \), \( \# \mathsf{Tang}_\beta = \# \mu \).

For each type index \( \beta \leq \alpha \), \( \# \mathsf{TSet}_\beta = \# \mu \).

Suppose that for all type indices \( \delta {\lt} \beta \), there are strictly less than \( \# \mu \)-many \( \delta \)-coding functions. Then there are less than \( \# \mu \) weak \( \beta \)-specifications.

Let \( \chi _1, \chi _2 \) be \( \beta \)-coding functions. If \( (S, x) \in \chi _1, \chi _2 \), then \( \chi _1 = \chi _2 \).

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) \).

Let \( S, T \) be supports such that \( T \) is strong and \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). If \( (N_1, N_3), (N_2, N_4) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), then \( N_1^\circ = N_2^\circ \) if and only if \( N_3^\circ = N_4^\circ \).

Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then \( \operatorname {\mathsf{conv}}_{S,T} \) is coherent.

Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then for each \( (N_1, N_3), (N_2, N_4) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\),

Let \( S, T \) be supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). If \( (a_1, a_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) and \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \).

Let \( S, T \) be supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is one-to-one.

Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then there is an allowable permutation \( \rho \) such that \( \rho (S) = T \).

If \( W \) is a weak specification that specifies supports \( S \) and \( T \), then there is an allowable permutation \( \rho \) such that \( \rho (S) = T \).

For every support \( S \), there is a strong support \( T \succeq S \).

Let \( S \) be a base support that is closed under interference of near-litters. Let \( a_1, a_2 \) be atoms not in \( \operatorname {\mathsf{im}}S^{\mathcal A}\) such that

Then there is a base permutation \( \pi \) that fixes \( S \) and maps \( a_1 \) to \( a_2 \).

Every support has a weak specification that specifies it.

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

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

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) \).

Let \( S, T \) be \( \beta \)-supports. Then \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \) if and only if ¹

• \( \operatorname {\mathsf{coim}}S_A^{\mathcal A}= \operatorname {\mathsf{coim}}T_A^{\mathcal A}\) and \( \operatorname {\mathsf{coim}}S_A^{\mathcal N}= \operatorname {\mathsf{coim}}T_A^{\mathcal N}\).

• (atom condition) Whenever \( (i, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2) \in T_A^{\mathcal A}\), we have

  \[ \forall j,\, (j, a_1) \in S_A^{\mathcal A}\leftrightarrow (j, a_2) \in T_A^{\mathcal A} \]

  and

  \[ \forall j,\, (\exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a_1 \in N) \leftrightarrow (\exists N,\, (j, N) \in T_A^{\mathcal N}\wedge a_2 \in N) \]

• (flexible condition) Whenever \( (i, N_1) \in S_A^{\mathcal N}\) and \( (i, N_2) \in T_A^{\mathcal N}\), if \( N_1^\circ \) is \( A \)-flexible, then so is \( N_2^\circ \), and

  \[ \forall j,\, (\exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N_1^\circ = {N’}^\circ ) \leftrightarrow (\exists N',\, (j, N') \in T_A^{\mathcal N}\wedge N_2^\circ = {N’}^\circ ) \]

• (inflexible condition) Let \( I = (\gamma ,\delta ,\varepsilon ) \) be an inflexible \( \beta \)-path and let \( t : \mathsf{Tang}_\delta \). Then whenever \( (i, N_1) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) and \( (i, N_2) \in T_{{A_\varepsilon }_\bot }^{\mathcal N}\) are such that \( N_1^\circ = f_{\delta ,\varepsilon }(t) \), there is some \( \delta \)-allowable permutation \( \rho \) such that \( N_2^\circ = f_{\delta ,\varepsilon }(\rho (t)) \), and

  \begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, \rho _B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\end{align*}

Let \( \rho \) be \( \beta \)-allowable, and let \( S \) be a \( \beta \)-support. Then \( \operatorname {\mathsf{spec}}(\rho (S)) = \operatorname {\mathsf{spec}}(S) \).

If \( S \) is a strong \( \beta \)-support and \( \rho \) is \( \beta \)-allowable, then \( \rho (S) \) is strong.

Let \( S \) be a base support that is closed under interference of near-litters. Suppose that \( S \) supports a set \( s : \operatorname {\mathsf{Set}}{\mathcal A}\) under the action of base permutations. Then for every pair of atoms \( a_1, a_2 \), the statements

and

imply that \( a_1 \in s \leftrightarrow a_2 \in s \).