Create a gist now

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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