TTFPHOAS.agda

data Proposition : Set where
  UNIT   : Proposition
  _=>_   : Proposition -> Proposition -> Proposition
  BOX    : Proposition -> Proposition

infixr 0 _=>_

postulate World : Set
          FIRST : World
          NEXT : World -> World

Context : Set1
Context = World -> Proposition -> Set

record IsProof (f : Context -> World -> Proposition -> Set) : Set1 where
  field
    var   : forall {cx w a} -> cx w a -> f cx w a
    unit  : forall {cx w} -> f cx w UNIT
    lam=> : forall {cx w a b} -> (cx w a -> f cx w b) -> f cx w (a => b)
    _$_   : forall {cx w a b} -> f cx w (a => b) -> f cx w a -> f cx w b
    box   : forall {cx w a} -> f cx (NEXT w) a -> f cx w (BOX a)
  infixl 0 _$_
  syntax lam=> (\a -> b) = lam a => b

Theorem : Proposition -> Set1
Theorem a = forall {f cx w} {{pf : IsProof f}} -> f cx w a

open IsProof {{...}} public

flip : forall {a b c} -> Theorem ((a => b => c) => (b => a => c))
flip = lam f => lam y => lam x => var f $ var x $ var y

nec : forall {a} -> Theorem a -> Theorem (BOX a)
nec x = box x