[Agda] Positivity checker

[Gyesik Lee]

Hi,

>The only
> reason such data types are permissible is because they can be defined by
> induction - so it makes sense to do so.

I think there is a general confusion between induction and recursion.
A function defined by recursion is based on an inductively defined
set, or in general on a well-founded relation.

Then, based on ZF set theory, one can show the existence of such a function.
If the positivity condition holds, so long as I know, Peter Aczel
showed that one can show the existence as a fixed point of an
inductive defintion.
Peter Dybjer made use of that idea too in one of his papers.
In general case, however, I know just proofs which can be found in any
standard set theory lecture notes.

Someone probably knows more than me.

And, in case of Data, I think, one has to consider it as a recursively
defined function based on natural numbers which is inductively
defined.

Gyesik