Dependencies

An atom is a pair \( a = (L, i) : {\mathcal L}\times \kappa \). ¹ The type of all atoms is denoted \( {\mathcal A}\), and \( \# {\mathcal A}= \# \mu \). We write \( (-)^\circ : {\mathcal A}\to {\mathcal L}\) for the operation \( (L, i) \mapsto L \). ² We write \( \operatorname {\mathsf{LS}}(L) :=\{ a \mid a^\circ = L \} \) for the litter set of \( L \). ³

A base permutation is a pair \( \pi = (\pi ^{\mathcal A}, \pi ^{\mathcal L}) \), where \( \pi ^{\mathcal A}\) is a permutation \( {\mathcal A}\simeq {\mathcal A}\) and \( \pi ^{\mathcal L}\) is a permutation \( {\mathcal L}\simeq {\mathcal L}\), such that

Base permutations have a natural group structure, they act on atoms by \( \pi ^{\mathcal A}\), they act on litters by \( \pi ^{\mathcal L}\), and they act on near-litters by ⁵

Base permutations are determined by their action on atoms. We should avoid directly referencing \( \pi ^{\mathcal A}\) and \( \pi ^{\mathcal L}\) whenever possible.

A base support is a pair \( S = (S^{\mathcal A}, S^{\mathcal N}) \) where \( S^{\mathcal A}\) is an enumeration of atoms and \( S^{\mathcal N}\) is an enumeration of near-litters. There are precisely \( \# \mu \) base supports.

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.

Let \( \tau \) be a type. An enumeration of \( \tau \) is a pair \( E = (i, f) \) where \( i : \kappa \) and \( f \) is a partial function \( \kappa \to \tau \), such that all domain elements of \( f \) are strictly less than \( i \). ² If \( x : \tau \), we write \( x \in E \) for \( x \in \operatorname {\mathsf{ran}}f \). The set \( \{ y \mid y \in E \} \), which we may also loosely call \( E \), is small. We will write \( \varnothing \) for the empty enumeration \( (0, \varnothing ) \).

If \( g : \tau \to \sigma \), then \( g \) lifts to a direct image function mapping enumerations of \( \tau \) to enumerations of \( \sigma \):

Thus, \( x \in g(E) \leftrightarrow x \in g[E] \). In the same way, groups that act on \( \tau \) also act on enumerations of \( \tau \). ³ If \( g : \sigma \to \tau \) is injective, then \( g \) lifts to an inverse image function mapping enumerations of \( \tau \) to enumerations of \( \sigma \):

This operation may cause the domain of \( f \) to shrink, but we will keep \( i \) the same.

If \( E = (i, e) \) and \( F = (j, f) \) are enumerations of \( \tau \), we define their concatenation by

This operation commutes with the others: \( x \in E + F \leftrightarrow x \in E \vee x \in F \), \( g[E + F] = g[E] + g[F] \), and \( g^{-1}[E + F] = g^{-1}[E] + g^{-1}[F] \).

We define a partial order on enumerations by setting \( (i, e) \leq (j, f) \) if and only if \( f \) extends \( e \) as a partial function. We obtain various corollaries, such as \( E \leq F \to g(E) \leq g(F) \) and \( E \leq E + F \).

Every small subset of \( \tau \) is the range of some enumeration of \( \tau \).

If \( \# \tau \leq \# \mu \), then there are at most \( \# \mu \)-many enumerations of \( \tau \): enumerations are determined by an element of \( \kappa \) and a small subset of \( \kappa \times \tau \). If \( \# \tau {\lt} \# \mu \), then there are strictly less than \( \# \mu \)-many enumerations of \( \tau \): use the same reasoning and apply lemma A.6.

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

A litter is a triple \( L = (\nu , \beta , \gamma ) : \mu \times \lambda ^\bot \times \lambda \) where \( \beta \neq \gamma \). The type of all litters is denoted \( {\mathcal L}\), and \( \# {\mathcal L}= \# \mu \).

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.

A near-litter is a pair \( N = (L, s) : {\mathcal L}\times \operatorname {\mathsf{Set}}{\mathcal A}\) such that \( s \mathrel {\overset {N}{\sim }}\operatorname {\mathsf{LS}}(L) \). ⁴ We write \( (-)^\circ : {\mathcal N}\to {\mathcal L}\) for the operation \( (L, s) \mapsto L \). We write \( a \in N \) for \( a \in s \), where \( N = (L, s) \). Near-litters satisfy extensionality: there is at most one choice of \( L \) for each \( s \). Each near-litter has size \( \# \kappa \) when treated as a set of atoms. The type of all near-litters is denoted \( {\mathcal N}\), and \( \# {\mathcal N}= \# \mu \) (there are \( \# \mu \) litters, and \( \# \mu \) small sets of atoms by lemma A.6; the latter observation should be its own lemma).

We have \( M \mathrel {\overset {N}{\sim }}N \) if and only if \( M^\circ = N^\circ \). If \( M^\circ = N^\circ \), then \( M \mathrel {\triangle }N \) is small and \( M \cap N \) has size \( \# \kappa \). If \( M^\circ \neq N^\circ \), then \( M \cap N \) has size \( \# \kappa \) and \( M \cap N \) is small.

A collection of model parameters is a tuple \( (\lambda , {{\lt}_\lambda }, \kappa , \mu ) \) such that

• \( {{\lt}} = {{\lt}_\lambda } \) is a well-order on \( \lambda \), and under this ordering, \( \lambda \) has no maximal element (so \( \operatorname {\mathsf{ot}}(\lambda ) \) is a limit ordinal);

• \( \# \kappa \) is uncountable and regular;

• \( \# \mu \) is a strong limit, and satisfies

  \[ \# \kappa {\lt} \# \mu ;\quad \# \kappa \leq \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu ));\quad \operatorname {\mathsf{ot}}(\lambda ) \leq \operatorname {\mathsf{ord}}(\operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu ))) \]

  so in particular, \( \operatorname {\mathsf{ot}}(\lambda ) \leq \operatorname {\mathsf{ord}}(\# \mu ) \). Note that the inequalities in \( \kappa \) are inequalities of cardinals; the inequality in \( \lambda \) is an inequality of ordinals.

Given a collection of model parameters, we define

• canonical well-orders on \( \kappa \) and \( \mu \) such that \( \operatorname {\mathsf{ot}}(\kappa ) = \operatorname {\mathsf{ord}}(\# \kappa ) \) and \( \operatorname {\mathsf{ot}}(\mu ) = \operatorname {\mathsf{ord}}(\# \mu ) \); and

• a canonical left-cancellative additive monoid on \( \kappa \), obtained by passing through the equivalence \( \kappa \simeq \{ o : \mathsf{Ord}\mid o {\lt} \operatorname {\mathsf{ord}}(\# \kappa ) \} \).

If \( \alpha , \beta \) are type indices, then a path \( \alpha \rightsquigarrow \beta \) is given by the constructors

• \( \operatorname {\mathsf{nil}} : \alpha \rightsquigarrow \alpha \);

• \( \operatorname {\mathsf{cons}} : (\alpha \rightsquigarrow \beta ) \to (\gamma {\lt} \beta ) \to (\alpha \rightsquigarrow \gamma ) \).

We define by recursion a \( \operatorname {\mathsf{snoc}} \) operation on the top of paths. We also prove the induction principle for \( \operatorname {\mathsf{nil}} \) and \( \operatorname {\mathsf{snoc}} \).

A path \( \alpha \rightsquigarrow \bot \) is called an \( \alpha \)-extended index. We write \( \operatorname {\mathsf{nil}}(\alpha ) \) for the path \( \{ \alpha \} : \alpha \rightsquigarrow \alpha \). If \( h \) is a proof of \( \beta {\lt} \alpha \), we write \( \operatorname {\mathsf{single}}(h) \) for the path \( \{ \alpha , \beta \} : \alpha \rightsquigarrow \beta \).

We have the inequality

Let \( \tau \) be a type. A position function for \( \tau \) is an injection \( \iota : \tau \to \mu \). This is a typeclass.

A set \( s : \operatorname {\mathsf{Set}}(\tau ) \) is called small if \( \# s {\lt} \# \kappa \). Smallness is stable under subset, intersection, small-indexed unions, symmetric difference, direct image, injective preimage, and many other operations (each of which should be its own lemma when formalised). Sets \( s, t : \operatorname {\mathsf{Set}}(\tau ) \) are called near if \( s \mathrel {\triangle }t \) is small; in this case, we write \( s \mathrel {\overset {N}{\sim }}t \). Nearness is an equivalence relation. If \( s \mathrel {\overset {N}{\sim }}t \) and \( u \) is small, then \( s \mathrel {\overset {N}{\sim }}(t \mathbin {\diamond } u) \), where \( \diamond \) is one of \( \cup , \cap , \setminus , \mathrel {\triangle }\).

Let \( \alpha \) be a type index. Then an \( \alpha \)-structural permutation (or just \( \alpha \)-permutation) is an \( \alpha \)-tree of base permutations. The type of \( \alpha \)-permutations is written \( \mathsf{StrPerm}_\alpha \).

The type of \( \alpha \)-structural sets, denoted \( \mathsf{StrSet}_\alpha \), is defined by well-founded recursion on \( \lambda ^\bot \).

• \( \mathsf{StrSet}_\bot :={\mathcal A}\);

• \( \mathsf{StrSet}_\alpha :=\prod _{\beta : \lambda ^\bot } \beta {\lt} \alpha \to \operatorname {\mathsf{Set}}\mathsf{StrSet}_\beta \) where \( \alpha : \lambda \).

These equalities will in fact only be equivalences in the formalisation. We define the action of \( \alpha \)-permutations (more precisely, inhabitants of some type with a \( \texttt{StrPermClass}_\alpha \) instance) on \( \alpha \)-structural sets by well-founded recursion.

• \( \pi (x) = \pi _{\operatorname {\mathsf{nil}}(\bot )}(x) \) if \( \alpha \equiv \bot \);

• \( \pi (x) = (\beta , h \mapsto \pi _h[x(\beta , h)]) \) if \( \alpha : \lambda \).

A \( \beta \)-structural support (or just \( \beta \)-support) is a pair \( S = (S^{\mathcal A}, S^{\mathcal N}) \) where \( S^{\mathcal A}\) is an enumeration of \( (\beta \rightsquigarrow \bot ) \times {\mathcal A}\) and \( S^{\mathcal N}\) is an enumeration of \( (\beta \rightsquigarrow \bot ) \times {\mathcal N}\). The type of \( \beta \)-supports is written \( \mathsf{StrSupp}_\beta \). There are precisely \( \# \mu \) structural supports for any type index \( \beta \).

For a path \( A : \beta \rightsquigarrow \bot \), we write \( S_A \) for the base support \( T \) given by

More generally, for a path \( A : \beta \rightsquigarrow \gamma \), we write \( S_A \) for the \( \gamma \)-support \( T \) given by

For a path \( A : \alpha \rightsquigarrow \beta \), we write \( S^A \) for the \( \alpha \)-support \( T \) given by

Clearly, \( (S^A)_A = S \).

\( \beta \)-structural permutations act on pairs \( (A, x) \) by \( \pi (A, x) = (A, \pi _A(x)) \), where \( x \) is either an atom or a near-litter. Hence, structural permutations act on structural supports.

Let \( \tau \) be a type, and let \( G \) be a \( \texttt{StrPermClass}_\beta \)-group that acts on \( \tau \). We say that \( S \) supports \( x : \tau \) under the action of \( G \) if whenever \( \pi : G \) fixes \( S \), it also fixes \( x \), and moreover, if \( \beta = \bot \) then \( S_A^{\mathcal N}\) is empty for any \( A : \bot \rightsquigarrow \bot \) (and of course there is exactly one such path).

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 \( \tau \) be any type, and let \( \alpha \) be a type index. An \( \alpha \)-tree of \( \tau \) is a function \( t \) that maps each \( \alpha \)-extended index \( A \) to an object \( t_A : \tau \); this defines its base derivatives. The type of \( \bot \)-trees of \( \tau \) is canonically isomorphic to \( \tau \). If \( t \) is an \( \alpha \)-tree and \( A : \alpha \rightsquigarrow \beta \), we define the derivative \( t_A \) to be the \( \beta \)-tree defined by \( (t_A)_B = t_{(A_B)} \). This derivative map is functorial: for any paths \( A : \alpha \rightsquigarrow \beta \) and \( B : \beta \rightsquigarrow \gamma \), we have \( t_{(A_B)} = (t_A)_B \). If \( \tau \) has a group structure, then so does its type of trees: \( (t \cdot u)_A = t_A \cdot u_A \) and \( (t^{-1})_A = (t_A)^{-1} \). If \( \tau \) acts on \( \upsilon \), then \( \alpha \)-trees of \( \tau \) act on \( \alpha \)-trees of \( \upsilon \): \( (t(u))_A = t_A(u_A) \).

If \( \# \tau \leq \# \mu \), there are at most \( \# \mu \)-many \( \alpha \)-trees of \( \tau \), since there are less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \)-many \( \alpha \)-extended indices, allowing us to conclude by lemma A.6 as each such tree is a subset of \( (\alpha \rightsquigarrow \bot ) \times \tau \) of size less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \). If \( \# \tau {\lt} \# \mu \), there are less than \( \# \mu \)-many \( \alpha \)-trees of \( \tau \), since there are less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \)-many \( \alpha \)-extended indices and strong limits are closed under exponentials.

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.

The type of type indices is \( \lambda ^\bot :=\texttt{WithBot}(\lambda ) \): the collection of proper type indices \( \lambda \) together with a designated symbol \( \bot \) which is smaller than all proper type indices. Note that \( \operatorname {\mathsf{ot}}(\lambda ^\bot ) = \operatorname {\mathsf{ot}}(\lambda ) \), and hence that for each \( \alpha : \lambda ^\bot \),

There are position functions on \( {\mathcal A}, {\mathcal N}\) that are jointly injective and satisfy

• \( \iota (\operatorname {\mathsf{NL}}(a^\circ )) {\lt} \iota (a) \) for every atom \( a \);

• \( \iota (\operatorname {\mathsf{NL}}(N^\circ )) \leq \iota (N) \) for every near-litter \( N \);

• \( \iota (a) {\lt} \iota (N) \) for every near-litter \( N \) and atom \( a \in N \mathrel {\triangle }\operatorname {\mathsf{LS}}(N^\circ ) \). ¹

We register these position functions as instances for use in typeclass inference. We also define \( \iota (L) = \iota (\operatorname {\mathsf{NL}}(L)) \) for litters.

Let \( \tau \) be a type such that \( \# \tau \leq \# \mu \). Let \( D : \tau \to \operatorname {\mathsf{Set}}(\mu ) \) be a function such that for each \( x : \tau \), the set \( D(x) \), called the denied set of \( x \), has size less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \). Then there is an injective function \( f : \tau \to \mu \) such that if \( \nu \in D(x) \), then \( \nu {\lt} f(x) \).

Let \( \beta \) be a type index with model data, and suppose that \( \mathsf{Tang}_\beta \) has a position function. Let \( \gamma \) be any proper type index not equal to \( \beta \). Then there is an injective fuzz map \( f_{\beta ,\gamma } : \mathsf{Tang}_\beta \to {\mathcal L}\) such that \( \iota (t) {\lt} \iota (f_{\beta ,\gamma }(t)) \), and the different \( f_{\beta ,\gamma } \) all have disjoint ranges. In particular, for any near-litter \( N \) with \( N^\circ = f_{\beta ,\gamma }(t) \), we have \( \iota (t) {\lt} \iota (N) \), and additionally, for any atom \( a \) with \( a^\circ = f_{\beta ,\gamma }(t) \), we have \( \iota (t) {\lt} \iota (a) \). ²

The tuple \( (\mathbb N, {{\lt}_{\mathbb N}}, \aleph _1, \beth _{\omega _1}) \) is a collection of model parameters, where the symbols \( \aleph _1 \) and \( \beth _{\omega _1} \) represent particular types of that cardinality.