Loeb's theorem

gistfile1.txt

module Loeb where

postulate
  □ : Set → Set
  L : Set → Set

unpack>t : Set → Set
unpack>t C = □ (□ (L C) → □ (□ (L C) → C))
unpack<t : Set → Set
unpack<t C = □ (□ (□ (L C) → C) → □ (L C))


A1t : Set → Set
A1t C = □ C → □ (□ C)

MPt : Set → Set → Set
MPt A B = □ (A → B) → □ A → □ B

postulate
  unpack> : {C : Set} → unpack>t C
  unpack< : {C : Set} → unpack<t C
  A1 : {C : Set} → A1t C
  A2 : {C : Set} → □ (A1t C)
  A3 : {A B : Set} → □ (MPt A B)
  MP : {A B : Set} → MPt A B
  B1 : {A B C : Set} → □ (A → B) → □ (B → C) → □ (A → C)
  B2 : {A B C : Set} → □ (A → B) → □ (A → B → C) → □ (A → C)

thm : {C : Set} → □ (□ C → C) → □ C
thm {C} s2 = s10 where
  ℓ = L C
  s3 : □ (□ (□ ℓ → C) → □ (□ ℓ) → □ C )
  s3 = A3 {□ (L C)} {C}
  s4 : □ (□ ℓ → □ (□ ℓ) → □ C)
  s4 = B1 unpack> s3
  s5 : □ (□ ℓ → □ (□ ℓ))
  s5 = A2 {ℓ}
  s6 : □ (□ ℓ → □ C)
  s6 = B2 s5 s4
  s7 : □ (□ ℓ → C)
  s7 = B1 s6 s2
  s8 : □ (□ (□ ℓ → C))
  s8 = A1 s7
  s9 : □ (□ ℓ)
  s9 = MP unpack< s8
  s10 : □ C
  s10 = MP s7 s9

thm2 : {C : Set} → □ (□ C → C) → □ C
thm2 s2 = MP s7 (MP unpack< (A1 s7)) where
  s7 = B1 (B2 A2 (B1 unpack> A3)) s2

(thm2 is just a syntactically more compact version of thm, names of axioms and steps come from http://yudkowsky.net/assets/44/LobsTheorem.pdf?1323322713 )