3.1 Codes and clouds
A code is a pair \( c = (\beta , s) \) where \( \beta {\lt} \alpha \) is a type index and \( s \) is a nonempty set of \( \mathsf{TSet}_\beta \).
The cloud relation \( \prec \) on codes is given by the constructor
where \( \beta , \gamma {\lt} \alpha \) are distinct and \( \gamma \) is proper.
If \( c \prec (\gamma , s_1) \) and \( c \prec (\gamma , s_2) \), then \( s_1 = s_2 \).
Let \( c = (\beta , s) \). We obtain
as required.
The cloud relation is injective (definition A.1). That is, if \( c_1, c_2 \prec d \), then \( c_1 = c_2 \).
Let \( c_i = (\beta _i, s_i) \) for \( i = 1, 2 \), and let \( d = (\gamma , s') \).
We first show that \( \beta _1 = \beta _2 \). Choose some \( t_1 : \mathsf{Tang}_{\beta _1} \) such that \( \operatorname {\mathsf{set}}(t_1) \in s_1 \). We can show directly that \( \operatorname {\mathsf{typed}}_\gamma (\operatorname {\mathsf{NL}}(f_{\beta _1,\gamma }(t_1))) \in s' \). So there is some \( t_2 : \mathsf{Tang}_{\beta _2} \) such that
Then since the typed near-litter map is injective (definition 2.24), the fact that the equations \( N^\circ = L_1 \) and \( N = \operatorname {\mathsf{NL}}(L_2) \) imply \( L_1 = L_2 \), and that the \( f \)-maps have disjoint ranges (proposition 2.22), we obtain \( \beta _1 = \beta _2 \).
We now show that if \( (\beta , s_1), (\beta , s_2) \prec d \), then \( s_1 \subseteq s_2 \). Let \( d = (\gamma , s') \) as above. Let \( x \in s_1 \), and choose \( t_1 : \mathsf{Tang}_\beta \) such that \( x = \operatorname {\mathsf{set}}(t_1) \). Then as \( (\beta , s_1) \prec d \), we have \( \operatorname {\mathsf{typed}}_\gamma (\operatorname {\mathsf{NL}}(f_{\beta ,\gamma }(t_1))) \in s' \). So there is some \( t_2 : \mathsf{Tang}_\beta \) with \( \operatorname {\mathsf{set}}(t_2) \in s_2 \) such that
For the same reasons as above, together with injectivity of \( f_{\beta ,\gamma } \), we have \( t_1 = t_2 \). In particular, \( x \in s_2 \) as required.
This gives the required result by antisymmetry.
The cloud relation is well-founded.
Define a function \( F \) that maps a code \( c = (\beta , s) \) to the set
We first show that \( c_1 \prec c_2 \) implies that
Let \( c_i = (\beta _i, s_i) \) for \( i = 1, 2 \), and suppose \( \nu _2 \in F(c_2) \). Then \( \nu _2 = \iota (t_2) \) with \( \operatorname {\mathsf{set}}(t_2) \in s_2 \). By definition, \( \operatorname {\mathsf{set}}(t_2) = \operatorname {\mathsf{typed}}_{\beta _2}(N) \) where \( N^\circ = f_{\beta _1,\beta _2}(t_1) \) and \( \operatorname {\mathsf{set}}(t_1) \in s_1 \). Then \( \iota (t_1) \in F(c_1) \), and \( \iota (t_1) {\lt} \iota (N) \leq \iota (t_2) \) by ??, as required.
Now, we define a function \( f \) that maps a code \( c \) to \( \min F(c) \), which is always well-defined as \( F(c) \) is nonempty. The above result shows that \( c_1 \prec c_2 \) implies \( f(c_1) {\lt} f(c_2) \). Thus \( \prec \) is a subrelation of the well-founded relation given by the inverse image of \( f \), so is well-founded.
Let \( \prec \) be a relation on a type \( \tau \). We say that an object \( x : \tau \) is \( \prec \)-even if all of its \( \prec \)-predecessors are odd; we say that \( x \) is \( \prec \)-odd if it has a \( \prec \)-predecessor that is even. Then:
Minimal objects are even.
If \( \prec \) is well-founded, then every object \( x : \tau \) is either even or odd, but not both.
Part 1. Direct from the definition.
Part 2. We show this by induction along \( \prec \). Suppose that all \( \prec \)-predecessors of \( x \) are either even or odd but not both. If all of these \( \prec \)-predecessors are odd, then \( x \) is even, and it is clearly not odd, because no \( y \prec x \) is even. Otherwise, there is \( y \prec x \) that is even, so \( x \) is odd, and it is not even because this \( y \) is not odd.
We define the relation \( \looparrowright \) between codes by the following two constructors.
If \( c \) is a \( \prec \)-even code, then \( c \looparrowright c \).
If \( c \) is a \( \prec \)-even code and \( c \prec d \), then \( c \looparrowright d \).
This relation is cofunctional (definition A.1): if \( d \) is a code, there is exactly one \( c \) such that \( c \looparrowright d \). Moreover, if \( c \looparrowright (\beta , s_1), (\beta , s_2) \), then \( s_1 = s_2 \).
If \( d \) is even, then \( d \looparrowright d \). If \( c \) is any other even code, \( c \nprec d \).
If \( d \) is odd, then there is an even code \( c \) with \( c \prec d \), so \( c \looparrowright d \). If \( c' \) is any other even code with \( c' \looparrowright d \), we must have \( c' \prec d \) as \( c' \) and \( d \) have different parities so cannot be equal, so \( c, c' \prec d \), so \( c = c' \) by proposition 3.4.
Finally, suppose \( c \looparrowright (\beta , s_1), (\beta , s_2) \). Suppose that \( c = (\beta , s_1) \). Then \( (\beta , s_1) \looparrowright (\beta , s_2) \) implies \( s_1 = s_2 \) because in the other constructor we may conclude \( \beta \neq \beta \). The same holds for \( c = (\beta , s_2) \) by symmetry. Now suppose that \( c \prec (\beta , s_1), (\beta , s_2) \). In this case, we immediately obtain \( s_1 = s_2 \) by proposition 3.3.
Let \( x : \mathsf{TSet}_\beta \) for some type index \( \beta {\lt} \alpha \), and let \( c \) be a code. We say that \( x \) is a type-\( \beta \) member of \( c \) if there is a set \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\beta \) such that \( x \in s \) and \( c \looparrowright (\beta , s) \), and hence for all sets \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\beta \) such that \( c \looparrowright (\beta , s) \), we have \( x \in s \) by definition 3.7. We write \( x \in _\beta c \). Note that this definition is only useful when \( c \) is even.
Let \( c_1, c_2 \) be even codes. If \( \beta {\lt} \alpha \) is a proper type index such that
then \( c_1 = c_2 \).
Suppose that there is no \( x : \mathsf{TSet}_\beta \) such that \( x \in _\beta c_1 \). Then it is easy to check that \( c_1 = (\gamma , \emptyset ) \) for some \( \gamma \), which is a contradiction as all codes are assumed to have nonempty second projections.
So there is some \( x : \mathsf{TSet}_\beta \) such that \( x \in _\beta c_1 \). Then there are sets \( s_1, s_2 \) where \( c_i \looparrowright (\beta , s_i) \) for \( i = 1, 2 \). Then, as \( x \in _\beta c_i \) holds if and only if \( x \in s_i \), we conclude \( s_1 = s_2 \). Hence \( c_1, c_2 \looparrowright (\beta , s_1) \), so as \( \looparrowright \) is injective, we conclude \( c_1 = c_2 \).