[Agda] Positivity checker

[Peter Hancock]

It occurred to me there *is* an inductive definition a bit like
Wouter's which has been rather well studied, and exhibits what
may be a similar kind of "negativity".

In the 60's logicians began to study systems they called ID_{< alpha},
where principle that takes you from A to T_A = mu X. 1 -> (A -> X)
is iterated a transfinite number of times, along a given wellordering
<, typically of order type w^w, or epsilon0.  So you would get a
predicate O : (a:Nat) -> (b:Nat) -> Set, where the first argument a
is really over the wellordering (here, coded in Nat), and the second b
is for things that satisfy the predicate O(a,_).  The crucial
thing is that the predicate O(a) is closed under some operation
whose operand has type \all n : Nat. O(a',n) -> O(a,{f}n), where a' < a.
-- in that case one would have O(a,2^a*3^a'*5^f). [{f}(_) is Kleene
application.]  Or something like that.

Now this is a bit messy and old-fashioned, and it would need some effort
to present it in a manner palatable to you youngsters.  But I mention
it in case someone (Peter?) will know what I am referring to, and can
make that effort more quickly than me. (The papers I am
thinking of straight off are by Feferman, Friedman, and are in the 1968
"Buffalo volume".)

In those (pre-universe) days, people didn't have much problem in
thinking of models of such (transfinitely iterated) g.i.d's.  But
perhaps the justification for them was really in terms of a recursive
definition along {<} into Set.

Hank