# The step to the next number class

By convention (since Cantor), the first number class is the set of natural numbers (or finite ordinals), the second is the set of ordinals which are at most countable (i.e. have cardinal at most that of the set of natural numbers), the third is the set of ordinals which have cardinal less than or equal to the set of countable ordinals, and so on.

In a typed calculus, the number classes can be represented by the following series of least fixed points:

• `Nat = NC0 = mu X. 1 + X`
• `NC1 = mu X. 1 + X + X^NC0`
• `NC2 = mu X. 1 + X + X^NC0 + X^NC1`
• `...`
How do we get rid of the `...` here and define the step from one number class to the next in a uniform way? (I am not interested here in dependent types, but only in simple types with no dependency. Nor do I care if the `first' number class turns out to be the second or the third -- it is only a matter of convention.)

The answer is to define instead the sequence of functors whose least fixed points are the various number classes. That is, we define a higher type operation:

```    Phi F X  = F X + X^(mu F)
```
and then consider the least fixed points of the series of functors `Id, Phi(Id), Phi^2(Id), ...`. Here `Id` stands for the identity functor `id(X) = X`.

Then the first number class is `0 = mu Id`, which is the empty set. The second is the least fixed point of ```X |-> Id(X) + X^0```, ie the set of natural numbers. The third is the set of countable ordinals, and so on.

The successive functors, and their initial algebras are as follows:

```
Functor B_n(X)            Initial algebra Omega_n = mu B_n
-------                   ---------------
Id X = X                  0 = Empty set
Maybe X = Id X + X^0      w = Natural numbers, first number class
B X = Id X + X^0 + X^w    W = Brouwer ordinals, second number class
...                       ...
```

I'd quite like to find a general description of this kind of construction in type-theory (particularly to look at collapsing functions from each number class starting at the third to its predecessor), and also to push beyond the finite number classes.

To make a start on this, try to define a collapsing function `theta_n : Omega_{n+1} -> Omega_n ` for `n > 1`. The idea is essentially this:

```      theta a = something like 1 + a
theta (L f) = (theta . f)^w (succ zero)
```
One needs the destination type to be at least the countable ordinals, so that one can define w-iteration of functions over it. Some pretty properties of theta are (not rigorously checked):
```  theta(Omega.a + b) = w^a + b
theta(Omega^(1+a).(1+b)) = phi_a b
```
provided we take the Veblen hierarchy `phi` to be based on `phi_0 b = w^(1+b)`. The collapsing function is order preserving on terms in Cantor Normal form to the base `Omega`. It is remarkable the way theta "lifts" multiplication to exponentiation, and exponentiation to iteration of the derivative operation.

Since Omega_n = mu B_n, we can reason:

```      theta_n : Omega_{n+1} -> Omega_n
= mu B_{n+1} -> mu B_n
= (mu X. B_n X + X^Omega_n) -> Omega_n
```
We can define `theta_n` to be the catamorphism ```iter f``` arising from an algebra ```f : B_n (Omega_n) + Omega_n ^ Omega_n```, and the most obvious inhabitant of that type is `[ constructors of Omega_n, omega-iteration]`. However, that is not quite what we want. We want to do something interesting with `zero', which is in a way a distinguished constructor.

To begin, maybe one should define some simple things.

```
emb_n : Omega_n -> Omega_{n+1}
emb_n = iterate (f : B_n Omega_{n+1} -> Omega_{n+1})
where f = cons_{n+1} . in_L

sup_n : (Omega_n -> Omega_{n+1}) -> Omega_{n+1}
sup_n = cons_{n+1} . in_R

lift_n : X -> B_n(X)
lift_0 = identity
lift_{n+1} = in_L . lift_n

```
Now we can define the sequence of initial ordinals -- for example 0, w = the first infinite ordinal, and "Church-Kleene" w_1 = the first uncountable ordinal. One simply takes for `w_n : Omega_{n+1}` the supremum `sup_{n+1} . emb_n`. Note that zero exists in every successor number-class, whereas successor exists in all number classes.

The problem now is to somehow break out "both ends" of the functors B_n. One wants to treat the first case (zero), and the last case (the new kind of supremum operation) specially in the definition of `theta`.

The idea of a universe of "higher order" functors, as opposed to a universe of sets is not new. Some other examples: universes of predicates over a fixed set of states, universes of relations or predicate transformers, universes of families, etc.

Peter Hancock