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

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

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

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

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