| 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 Ψ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment