[Agda] Forget Hurken's Paradox, Agda has a quicker route to success
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Sep 6 17:21:50 CEST 2012
{-# 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.
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/
More information about the Agda
mailing list