Let \( \alpha \) be a type index. Model data at type \( \alpha \) consists of: ¹

• a \( \mathsf{TSet}_\alpha \) called the type of tangled sets or t-sets, which will be our type of model elements at level \( \alpha \), with an embedding \( U_\alpha : \mathsf{TSet}_\alpha \to \mathsf{StrSet}_\alpha \);

• a group \( \mathsf{AllPerm}_\alpha \) called the type of allowable permutations, with a \( \texttt{StrPermClass}_\alpha \) instance and a specified action on \( \mathsf{TSet}_\alpha \),

such that

• if \( \rho : \mathsf{AllPerm}_\alpha \) and \( x : \mathsf{TSet}_\alpha \), then \( \rho (U_\alpha (x)) = U_\alpha (\rho (x)) \);

• every t-set of type \( \alpha \) has an \( \alpha \)-support (definition 2.15) for its action under the \( \alpha \)-allowable permutations.

Let \( \alpha \) be a type index with model data. An \( \alpha \)-tangle is a pair \( t = (x, S) \) where \( x \) is a tangled set of type \( \alpha \) and \( S \) is an \( \alpha \)-support for \( x \). We define \( \operatorname {\mathsf{set}}(t) = x \) and \( \operatorname {\mathsf{supp}}(t) = S \). The type of \( \alpha \)-tangles is denoted \( \mathsf{Tang}_\alpha \). Allowable permutations \( \rho \) act on tangles by \( \rho ((x, S)) = (\rho (x), \rho (S)) \), and so \( \operatorname {\mathsf{supp}}(t) \) supports \( t \) for its action under the allowable permutations. Therefore, each tangled set \( x \) is of the form \( \operatorname {\mathsf{set}}(t) \) for some tangle \( t \).

Let \( \alpha \) be a proper type index. Suppose that we have model data for all type indices \( \beta \leq \alpha \) and position functions for \( \mathsf{Tang}_\beta \) for all \( \beta {\lt} \alpha \). For any type index \( \beta \leq \alpha \), a inflexible \( \beta \)-path is a tuple \( I = (\gamma , \delta , \varepsilon , A) \) where \( \delta , \varepsilon {\lt} \gamma \) are distinct, the index \( \varepsilon \) is proper, and \( A : \beta \rightsquigarrow \gamma \). We will write \( \gamma _I, \delta _I, \varepsilon _I, A_I \) for its fields. Inflexible paths have a coderivative operation, given by \( (\gamma , \delta , \varepsilon , A)^B = (\gamma , \delta , \varepsilon , A^B) \).

Let \( \alpha \) be a proper type index with model data, and suppose that \( \mathsf{Tang}_\alpha \) has a position function. We say that \( \alpha \) has typed near-litters if there is an embedding \( \operatorname {\mathsf{typed}}_\alpha : {\mathcal N}\to \mathsf{TSet}_\alpha \) such that

• if \( \rho : \mathsf{AllPerm}_\alpha \) and \( N : {\mathcal N}\), then \( \rho (\operatorname {\mathsf{typed}}_\alpha (N)) = \operatorname {\mathsf{typed}}_\alpha (\rho _\bot (N)) \); and

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

Objects of the form \( \operatorname {\mathsf{typed}}_\alpha \) are called typed near-litters.

Let \( \alpha \) be a proper type index. Suppose that we have model data for all type indices \( \beta \leq \alpha \), position functions for \( \mathsf{Tang}_\beta \) for all \( \beta {\lt} \alpha \), and typed near-litters for all \( \beta {\lt} \alpha \). We say that the model data is coherent below level \( \alpha \) if the following hold.

• For \( \gamma {\lt} \beta \leq \alpha \), there is a map \( \mathsf{AllPerm}_\beta \to \mathsf{AllPerm}_\gamma \) that commutes with the coercions from \( \mathsf{AllPerm}_{(-)} \) to \( \mathsf{StrPerm}_{(-)} \). We can use this map to define arbitrary derivatives of allowable permutations by recursion on paths.

• If \( (x, S) \) is a \( \beta \)-tangle for \( \beta {\lt} \alpha \), and \( y \) is an atom or near-litter that occurs in the range of \( S_A \), then \( \iota (y) {\lt} \iota (x, S) \).

• Let \( \beta \leq \alpha \), and let \( \gamma , \delta {\lt} \beta \) be distinct with \( \delta \) proper. Let \( t : \mathsf{Tang}_\gamma \) and \( \rho : \mathsf{AllPerm}_\beta \). Then

  \[ (\rho _\delta )_\bot (f_{\gamma ,\delta }(t)) = f_{\gamma ,\delta }(\rho _\gamma (t)) \]

  In particular, for every \( \beta \leq \alpha \), \( \beta \)-allowable permutation \( \rho \), and \( \beta \)-inflexible path \( I \), we obtain

  \[ ((\rho _A)_\varepsilon )_\bot (f_{\delta ,\varepsilon }(t)) = f_{\delta ,\varepsilon }((\rho _A)_\delta (t)) \]

  where subscripts of \( I \) are suppressed.

• Suppose that \( \beta \leq \alpha \) and \( (\rho (\gamma ))_{\gamma {\lt} \beta } \) is a collection of allowable permutations such that whenever \( \gamma , \delta {\lt} \beta \) are distinct, \( \delta \) is proper, and \( t : \mathsf{Tang}_\delta \), we have

  \[ (\rho (\delta ))_\bot (f_{\gamma ,\delta }(t)) = f_{\gamma ,\delta }(\rho (\gamma )(t)) \]

  Then there is a \( \beta \)-allowable permutation \( \rho \) with \( \rho _\gamma = \rho (\gamma ) \) for each \( \gamma {\lt} \beta \).

• If \( \beta \leq \alpha \) is a proper type index and \( x : \mathsf{TSet}_\beta \), then for any \( \gamma {\lt} \beta \),

  \[ U_\beta (x)(\gamma ) \subseteq \operatorname {\mathsf{ran}}U_\gamma \]

• (extensionality) If \( \beta , \gamma \leq \alpha \) are proper type indices where \( \gamma {\lt} \beta \), the map \( U_\beta (-)(\gamma ) : \mathsf{TSet}_\beta \to \operatorname {\mathsf{Set}}\mathsf{StrSet}_\gamma \) is injective.

• If \( \beta , \gamma : \lambda \) where \( \gamma {\lt} \beta \), for every \( x : \mathsf{TSet}_\gamma \) there is some \( y : \mathsf{TSet}_\beta \) such that \( U_\beta (y)(\gamma ) = \{ x \} \). We write \( \operatorname {\mathsf{singleton}}_\beta (x) \) for this object \( y \), which is uniquely defined by extensionality.

Note that this structure contains data (the derivative maps for allowable permutations and the singleton operations), but the type is a subsingleton: any two inhabitants are propositionally equal. We will not use this fact directly, but the idea will have relevance in chapter 6.