[Agda] Size change of higher order arguments

[Peter Dybjer]

> Dear Shin-Cheng,
>
> what Nisse has answered you is all correct.  It makes sense to think of
> a whole function to be bigger than one of it's value:
>
>     f a <= f
>
> This is sound for predicative type theories.  The idea is by Thierry
> (Pattern matching ..., TYPES 92) and there is a formal proof of
> well-foundedness by Thorsten and me in the paper cited below (JFP 02).

Just a historial remark. The notion of structural recursion over a
generalized inductive definition like the Brouwer ordinals is much older
than that, maybe Brouwer had it already. It is in Scott's "Constructive
Validity" version of dependent type theory from 1970 for example.

What is new in Thierry's paper is the idea to generalize the notion of
terminating recursion which is expressed by elimination
rules/primitive(structural) recursive schemata, to a more general notion
of "structurally smaller recursion" together with "pattern matching on
dependent types".

Peter