Issue690.agda

{-# OPTIONS --type-in-type #-}
-- {-# OPTIONS -v tc.pos:10 -v tc.polarity:10 #-}
-- Andreas, 2012-09-06, message on Agda list "Forget Hurken's paradox..."

module Issue690 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