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