Hurkens.agda

{-# OPTIONS --type-in-type  #-}

module Hurkens where

-----------------------

O = Set

Bottom : O
Bottom = (A : O) → A

Not : O → O
Not X = X → Bottom

P : O → O
P A = A → O

P/ : {X Y : O} → (X → Y) → (P Y → P X)
P/ f py x = py (f x)

PP : O → O
PP X = P (P X)

PP/ : {X Y : O} → (X → Y) → (PP X → PP Y)
PP/ f = P/ (P/ f)

Alg : O → O
Alg X = PP X → X

-----------------------

U : O
U = ∀ {X} → Alg X → PP X

V : O
V = P U

-- algebra operation over U
mk : Alg U
mk ppu alg px = ppu \u → px (alg (u alg))

-- closure in U
U[_] : U → U
U[ u ] = mk (u mk)

-- closure for subsets of U
V[_] : V → V
V[_] = P/ U[_]

-----------------------

U' : P U
U' u = (v : V) → u mk v → V[ v ] u

V' : P V
V' v = (u : U) → u mk v → v u

-- closure in U'
U'[_] : {u : U} → U' u → U' U[ u ]
U'[ u' ]  v = u' V[ v ]

-- closure in V'
V'[_] : {v : V} → V' v → V' V[ v ]
V'[ v' ]  u = v' U[ u ]

-----------------------

u0 : U
u0 = mk V'
-- u0 mk v = V' V[ v ]

OK : (v : V) → V' v → v u0
OK _ v' = v' u0 V'[ v' ]

u0' : U' u0
u0' v = OK V[ v ]

-----------------------

v0 : V
v0 u = Not (U' u)

v0' : V' v0
v0' u u/v0 u' = u' v0 u/v0 (U'[_] {u} u')

-----------------------

bottom : Bottom
bottom = OK v0 v0' u0'