Lob.agda

module Lob where

open import Data.Product
open import Function

_←→_ : Set → Set → Set
A ←→ B = (A → B) × (B → A)

postulate -- provability axioms
  □ : Set → Set
  ev : ∀ {A} → A → □ A
  a3 : ∀ {A B} → □ (A → B) → □ A → □ B

postulate -- Assuming fixed point theorem
  fp : (F : Set → Set) → Σ[ Q ∈ Set ] (F (□ Q) ←→ Q)

_<$>_ : ∀ {A B} → (A → B) → □ A → □ B
f <$> x = a3 (ev f) x

infix 1 _<$>_

lob : ∀ P → (□ P → P) → P
lob P prf with fp (λ X → X → P)
lob P prf | ψ , ψ₁ , ψ₂ = ψ→P $ ψ₁ λ □ψ → prf $ ψ→P <$> □ψ
  where ψ→P : ψ → P
        ψ→P Ψ = ψ₂ Ψ (ev Ψ)