[Agda] Positivity checker

[Peter Dybjer]

On Dec 5, 2008, at 4:53 PM, Nils Anders Danielsson wrote:

> On 2008-12-04 17:31, Wouter Swierstra wrote:
>> When I define the following data type in Agda, the positivity  
>> checker complains:
>> data Data : Nat -> Set where
>>  Base : Data Zero
>>  Step : forall {n} -> (Data n -> Data n) -> Data (Succ n)
>> This declaration reeks of negativity, but on closer inspection it  
>> shouldn't really be a problem. The index limits the amount of  
>> recursion that can be done.
>
> I argued in a similar way in "A Formalisation of a Dependently Typed
> Language as an Inductive-Recursive Family".

The reason why this data type is ok, is because it is isomorphic to  
the corresponding family defined by induction on n.

But what is the induction principle? Except induction on n?

>> but I'd much rather work with data (the example I have in mind is
>> pretty complicated).
>
> Yes.

Why?

Peter