[Agda] Simple contradiction from type-in-type

[Andreas Abel]

Beautiful, added this to test/succeed/.

On 15.03.13 8:03 AM, Dominique Devriese wrote:
> In that referenced discussion, Paolo Capriotti links to this code:
>
>    http://hpaste.org/84029
>
> This paradox seems to require type-in-type and inductive data types
> and was simpler and more understandable than any other I had already
> seen.
>
> Dominique
>
> 2013/3/14 Andreas Abel <andreas.abel at ifi.lmu.de>:
>> Samuel, this paradox was discovered and fixed in September...
>> Cheers, Andreas
>>
>> Thu Sep 13 09:52:35 CEST 2012  Andreas Abel <andreas.abel at ifi.lmu.de>
>>    * Fixed a bug in the positivity analysis for data type indices.
>>
>> -------- Original Message --------
>> Subject: Forget Hurken's Paradox, Agda has a quicker route to success
>> Date: Thu, 06 Sep 2012 17:21:50 +0200
>> From: Andreas Abel <andreas.abel at ifi.lmu.de>
>> To: Agda List <Agda at lists.chalmers.se>
>>
>>    {-# OPTIONS --type-in-type #-}
>>    module ForgetHurkens where
>>
>>    infix 4 _≡_
>>
>>    data _≡_ {A : Set} (x : A) : A → Set where
>>      refl : x ≡ x
>>
>>    data ⊥ : Set where
>>
>>    data D : Set where
>>      abs : ∀ {E : Set} → D ≡ E → (E → ⊥) → D
>>
>>    lam : (D → ⊥) → D
>>    lam f = abs refl f
>>
>>    app : D → D → ⊥
>>    app (abs refl f) d = f d
>>
>>    omega : D
>>    omega = lam (λ x → app x x)
>>
>>    Omega : ⊥
>>    Omega = app omega omega
>>
>> The problem is that Agda considers
>>
>>    F D = \Sigma E : Set. (D ≡ E) * (E → ⊥)
>>
>> as strictly positive in D.  Funnily, it complains when I swap the
>> arguments to equality; the same thing with E ≡ D is rejected (correctly).
>>
>> Note: I am not using the full Set : Set, just an impredicative Set.
>>
>> If I try the same in Coq, it is rejected because the definition of D is
>> not considered strictly positiv.
>>
>>    Inductive Id {A : Type} (x : A) : A -> Prop :=
>>    | refl : Id x x.
>>
>>    Definition cast {P Q : Prop}(eq : Id P Q) : P -> Q :=
>>      match eq with
>>      | refl => fun x => x
>>      end.
>>
>>    Inductive False : Prop :=.
>>
>>    Inductive D : Prop :=
>>    | abs : forall (E : Prop), Id D E -> (E -> False) -> D.
>>
>>    Definition lam (f : D -> False) : D := abs D (refl D) f.
>>    Definition app (f : D) (d : D) : False :=
>>      match f with
>>      | abs E eq g => g (cast eq d)
>>      end.
>>
>>    Definition omega : D     := lam (fun x => app x x).
>>    Definition Omega : False := app omega omega.
>>
>>
>>
>> On 14.03.2013 15:37, Dominique Devriese wrote:
>>>
>>> Samuel,
>>>
>>> 2013/3/14 Samuel Gélineau <gelisam at gmail.com>:
>>>>
>>>>       data Con : Set where
>>>>         -- curry's paradox would use this.
>>>>         --   mkCon : (Con → ⊥) → Con
>>>>         -- since we have type-in-type but not negative occurrences,
>>>>         -- fake it using propositional equality.
>>>>         con : (A : Set) → Con ≡ A → (A → ⊥) → Con
>>>
>>>
>>> Interesting!  But actually, the above does not seem to be accepted by
>>> the latest (darcs) version of Agda, even when I specify to allow
>>> type-in-type.  I need to also turn off the positivity checker, despite
>>> what your comment suggests.
>>>
>>> Regards,
>>> Dominique

-- 
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/