{-# OPTIONS --type-in-type --without-K #-}
module burali where

Prop' = Set

power : Set → Set
power X = X → Prop'

∃ : (A : Set) → (A → Prop') → Prop'
∃ A B = {X : Prop'} → ((a : A) → B a → X) → X

_,_ : {A : Set}{B : A → Prop'}
    → (a : A) → B a → ∃ A B
_,_ a b {X} f = f a b
infixr 4 _,_

_≡_ : {A : Set} → A → A → Prop'
_≡_ {A} x y = (P : A → Prop') → P x → P y

refl : {A : Set}{x : A} → x ≡ x
refl P u = u

¬_ : Prop' → Prop'
¬ A = {X : Prop'} → A → X

_∧_ : Prop' → Prop' → Prop'
A ∧ B = ∃ A (λ _ → B)

image : {A B : Set} → (A → B) → power A → power B
image {A}{B} f V b = ∃ A λ a → (V a) ∧ (f a ≡ b)

U : Set
U = (X : Set) → (power X → X) → power X

τ : power U → U
τ V X r = image (λ k → r (k X r)) V

σ : U → power U
σ k = k U τ

_<_ : U → U → Set
x < y = σ y x

ind : power U → Prop'
ind V = (x : U) → ((y : U) → y < x → V y) → V x

dec : U → Prop'
dec x = {V : power U} → ind V → V x

Ω : U
Ω = τ dec

absurd : (A : Prop') → A
absurd = Ω-dec Z-ind (Ω , λ {X} f → f Ω-dec refl)
  where
    pre-ind : {X : power U} → ind X
            → ind (λ x → X (τ (σ x)))
    pre-ind {X} i x h = i (τ (σ x)) λ y p
      → p λ z l-eq
      → l-eq λ l eq
      → eq X (h z l)

    Ω-dec : dec Ω
    Ω-dec {X} i = i Ω λ x p
      → p λ w d-eq
      → d-eq λ d eq
      → eq X (d (pre-ind i))

    Z : power U
    Z y = ¬ (τ (σ y) < y)

    Z-ind : ind Z
    Z-ind x h n = h (τ (σ x)) n
      (τ (σ x) , λ {X} f → f n refl)