2.4 Position functions
Let \( \tau \) be a type. A position function for \( \tau \) is an injection \( \iota : \tau \to \mu \). This is a typeclass.
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) \).
Pick a well-ordering \( \prec \) of \( \tau \) of length at most \( \operatorname {\mathsf{ord}}(\# \mu ) \). Define \( f \) by well-founded recursion on \( \prec \). Suppose that we have already defined \( f \) for all \( y \prec x \). Then let
This set has size strictly less than \( \mu \), so there is some \( \nu : \mu \) not contained in it. Set \( f(x) = \nu \).
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 ) \). 1
We register these position functions as instances for use in typeclass inference. We also define \( \iota (L) = \iota (\operatorname {\mathsf{NL}}(L)) \) for litters.
First, establish an equivalence \( f_{\mathcal L}: {\mathcal L}\simeq \mu \). Use proposition 2.18 to obtain an injective map \( f_{\mathcal A}: {\mathcal N}\to \mu \) such that \( f_{\mathcal L}(a^\circ ) {\lt} f_{\mathcal A}(a) \) for each atom \( a \). Now use proposition 2.18 again to obtain an injective map \( f_{\mathcal N}: {\mathcal N}\to \mu \) such that
Endow \( 3 \times \mu \) with its lexicographic order, of order type \( \operatorname {\mathsf{ord}}(\# \mu ) \), giving an order isomorphism \( e : 3 \times \mu \simeq \mu \). Finally, we define