open data ⊤ | tt
open data ⊥

open data Con : Type
  | •
  | infix ▷ Con Ty

open data Ty : Type
  | infixr ‘→’ Ty Ty
  | ‘⊤’
  | ‘⊥’
  | ‘□’ Ty

open data Tm (Γ : Con) Ty : Type
  | Γ,     A ‘→’ B         ⇒ lam (Tm (Γ ▷ A) B)
  | Γ ▷ A, B               ⇒ app (Tm Γ (A ‘→’ B))
  | Γ,     ‘⊤’             ⇒ ‘tt’
  | •,     P               ⇒ Löb (Tm • (‘□’ P ‘→’ P))

def □ ⇒ Tm •

def interpTy (A : Ty) : Type
  | ‘⊤’     ⇒ ⊤
  | ‘⊥’     ⇒ ⊥
  | ‘□’ P   ⇒ □ P
  | A ‘→’ B ⇒ interpTy A → interpTy B

def interpCon (Γ : Con) : Type
  | •     ⇒ ⊤
  | Γ ▷ A ⇒ Σ (interpCon Γ) ** (interpTy A)

def interpTm {Γ : Con} {T : Ty} (t : Tm Γ T) (ic : interpCon Γ) : interpTy T
  | lam f,   Γᵥ      ⇒ fn a ⇒ (interpTm f (Γᵥ, a))
  | app f,   (Γᵥ, a) ⇒ (interpTm f Γᵥ) a
  | ‘tt’,    Γᵥ      ⇒ tt
  | Löb f,   tt      ⇒ interpTm f tt (Löb f)

def fixl ¬   (A : Type) : Type ⇒ A → ⊥
def fixl ‘¬’ (A : Ty)   : Ty   ⇒ A ‘→’ ‘⊥’

def consistent : ¬ □ ‘⊥’
  ⇒ fn false ⇒ interpTm false tt
def incomplete : ¬ □ (‘¬’ (‘□’ ‘⊥’))
  ⇒ fn lob ⇒ interpTm (Löb lob) tt