[Agda] Ordinals in Agda

[Martin Escardo]

In my work advertised earlier, I transfinitely iterated an operation of 
countable arity in order to get arbitrarily complex omniscient sets in 
constructive mathematics (and Agda in particular).

This time I want to advertise cool work by Coquand, Hancock and Setzer 
that constructs incredibly large ordinals in a neat way, using Church 
encodings of ordinals and lenses. These encodings are nothing but the 
transfinite iterators of the ordinals they encode.

Here I content myself with defining basic arithmetic on ordinals 
(addition, multiplication and exponentiation), so that an ordinal that 
cannot be defined in Goedel's system T becomes definable in Martin-Loef 
type theory, and hence Agda, thanks to the use of a universe and 
dependent types:

     http://www.cs.bham.ac.uk/~mhe/papers/ordinals/ordinals.html

If you want to see really large ordinals, use lenses, available free of 
charge at Hanck's web page

     http://personal.cis.strath.ac.uk/~ph/

which includes several interesting writings and programs in (the 
previous version of) Agda and in Haskell.

Hanck's lenses work like a binocular used the other way round: they make 
huge things look tiny.

You may ask why the above authors care. In proof theory, one uses 
ordinals to measure the strength of formal logical systems. Here they 
are using them to measure the expressivity of programming languages. If 
you get (Church encodings of) larger ordinals, you also get more 
functions N->N. In particular, Agda defines many more functions N->N 
than Goedel's system T.

Martin