Girard-Hurkens paradox in Agda

Hurkens.agda

{-# OPTIONS --rewriting --confluence-check #-}

module Hurkens where

open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite

postulate
  Π₁ : (Set₁ → Set₁) → Set₁
  λ₁ : ∀ {F} → (∀ A → F A) → Π₁ F
  _[_]₁ : ∀ {F} → Π₁ F → ∀ A → F A
  β₁ : ∀ {F} f A → λ₁ {F = F} f [ A ]₁ ≡ f A

  Π₀ : (A : Set₁) → (A → Set) → Set
  λ₀ : ∀ {A B} → (∀ x → B x) → Π₀ A B
  _[_]₀ : ∀ {A B} → Π₀ A B → ∀ x → B x

{-# REWRITE β₁ #-}

𝒫_ : Set₁ → Set₁
𝒫 S = S → Set

U : Set₁
U = Π₁ λ A → (𝒫 𝒫 A → A) → 𝒫 𝒫 A

τ : 𝒫 𝒫 U → U
τ t = λ₁ λ X f p → t λ x → p (f ((x [ X ]₁) f))

σ : U → 𝒫 𝒫 U
σ s = (s [ U ]₁) τ

ind : 𝒫 𝒫 U
ind X = Π₀ U λ x → σ x X → X x

wf : ∀ X → ind X → X (τ ind)
wf X hX = (hX [ τ ind ]₀) (λ₀ λ x hx → (hX [ _ ]₀) hx)

⊥ : ∀ A → A
⊥ A = wf
  (λ y → (Π₀ (𝒫 U) (λ X → σ y X → X (τ (σ y)))) → A)
  (λ₀ λ x hx h → (h [ _ ]₀) hx (λ₀ λ X → h [ _ ]₀))
  (λ₀ λ X → wf _)