[Agda] Positivity checker

[Gyesik Lee]

> I find your arguments for prefering inductively to recursively defined
> families interesting, but hardly conclusive. My own feeling is that it
> depends on the situation which is better. For cases like Vec, the inductive
> one is a "generator" and the recursive one simplifies.

I agree. My experience with Coq tells me it really depends on the
situation whether you should choose for an inductive definition or for
a recursive function, of course when you have both options.