[Agda] More universe polymorphism

[Martin Escardo]

On 28/06/13 10:28, Nils Anders Danielsson wrote:
> On 2013-06-28 01:09, Darryl McAdams wrote:
>> I've certainly run into issues with levels. A good example is an
>> implementation of Scott/Church encodings. You can define the encoding,
>> but trying to define simple things like addition becomes difficult if
>> not impossible, from what I can tell.
>
> Are you referring to some kind of universe-polymorphic Church numerals?
> The basic encoding works fine (for addition, at least):

However, you will run into problems if you want to work with Church 
numerals without using an existing type of inductively defined natural 
numbers as in your Agda code. The reason is that the recursor of the 
inductively defined natural numbers has a more general type than the 
recursor for Church numerals can have in general.

For example, it has been proven that in the simply typed lambda calculus 
with one (unspecified) ground type, the exponential function is not 
definable wrt Church encoding.

Best,
Martin