Hurkens' paradox in Agda using Impredicativity

Hurkens.agda

module Hurkens where

-- derived from https://github.com/agda/agda/blob/5d30d8e7a25dfced02edefd82699f1f7b6f79316/test/Succeed/Hurkens.agda
-- adapted to use impredicativity instead of --type-in-type

data ⊥ : Set where

{-# NO_UNIVERSE_CHECK #-}
record Impred₁ (A : Set₂) (B : A → Set₁) : Set₁ where
  field at : (a : A) → B a
{-# NO_UNIVERSE_CHECK #-}
record Impred₀ (A : Set₁) (B : A → Set) : Set where
  field at : (a : A) → B a

¬_ : Set → Set
¬ A = A → ⊥

P : Set₁ → Set₁
P A = A → Set

U : Set₁
U = Impred₁ Set₁ λ X → (P (P X) → X) → P (P X)

τ : P (P U) → U
τ t .Impred₁.at X f p = t λ x → p (f (x .Impred₁.at X f))

σ : U → P (P U)
σ s = s .Impred₁.at U λ t → τ t

Δ : P U
Δ y = ¬ (Impred₀ (P U) λ p → σ y p → p (τ (σ y)))

Ω : U
Ω = τ λ p → Impred₀ U λ x → σ x p → p x

D : Set
D = Impred₀ (P U) λ p → σ Ω p → p (τ (σ Ω))

lem₁ : (p : P U) → ((x : U) → σ x p → p x) → p Ω
lem₁ p H1 = H1 Ω record { at = λ x → H1 (τ (σ x)) }

lem₂ : ¬ D
lem₂ = lem₁ Δ λ x H2 H3 → H3 .Impred₀.at Δ H2 record { at = λ p → H3 .Impred₀.at λ y → p (τ (σ y)) }

lem₃ : D
lem₃ .Impred₀.at p H1 = lem₁
  (λ y → p (τ (σ y)))
  (H1 .Impred₀.at)

loop : ⊥
loop = lem₂ lem₃