[Agda] Forget Hurken's Paradox, Agda has a quicker route to success

[Andreas Abel]

On 06.09.12 10:52 PM, Andrés Sicard-Ramírez wrote:
> On Thu, Sep 6, 2012 at 12:25 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>>
>> I have a fix for this (filed as issue 690), that looks also for occurrences
>> in the indices.
>
> FYI, using that fix the following data type (previously accepted) is
> rejected by Agda (and Coq)
>
> data T : Set → Set where
>    c : T (T ℕ)

That seems to be a good thing.  Trying to make sense of T in terms of 
inductive types, explaining indices via equalities, one arrives at

   data T (X : Set) : Set where
     c : (X == T N) -> T X

which has a non-positive occurrence of T in (X == T N).

An argument for the existence of T would have to argue for the existence 
this least fixed point:

   lfp \lambda T X -> (X == T N)

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/