5.2 Coding functions
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. 1
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 \( \chi _1, \chi _2 \) be \( \beta \)-coding functions. If \( (S, x) \in \chi _1, \chi _2 \), then \( \chi _1 = \chi _2 \).
We show \( \chi _1 \subseteq \chi _2 \); the result then follows by antisymmetry. Suppose \( (T, y) \in \chi _1 \). Then \( T = \rho (S) \) for some \( \beta \)-allowable \( \rho \). As \( (\rho (S), \rho (x)) \in \chi _1 \) and \( \chi _1 \) is coinjective, we obtain \( y = \rho (x) \). Hence \( (T, y) \in \chi _2 \) as required.
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 \).
If \( \rho (t) = u \), then \( (\operatorname {\mathsf{supp}}(t), \operatorname {\mathsf{set}}(t)) \in \chi _t \) implies \( (\operatorname {\mathsf{supp}}(u), \operatorname {\mathsf{set}}(u)) \in \chi _t \), giving \( \chi _t = \chi _u \) by proposition 5.7. Conversely if \( \chi _t = \chi _u \), then \( (\operatorname {\mathsf{supp}}(u), \operatorname {\mathsf{set}}(u)) \in \chi _t \), so there is \( \rho \) such that \( \rho (\operatorname {\mathsf{supp}}(t)) = \operatorname {\mathsf{supp}}(u) \), and \( (\rho (\operatorname {\mathsf{supp}}(t)), \rho (\operatorname {\mathsf{set}}(t))) \in \chi _t \), so by coinjectivity we obtain \( \rho (set(t)) = \operatorname {\mathsf{set}}(u) \) as required.