[Agda] Simple contradiction from type-in-type

[Dominique Devriese]

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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> --
> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda