Goedel's 2nd theorem from Loeb's

goedel.idr

-- https://mathoverflow.net/questions/272982/how-do-we-construct-the-g%C3%B6del-s-sentence-in-martin-l%C3%B6f-type-theory
-- Top/TT is unnecessary here actually 

module LobToGoedel

import Data.List.Elem

%default total

data Ty : Type where
  Imp : Ty -> Ty -> Ty
  Top : Ty
  Bot : Ty
  Box : Ty -> Ty

NotI : Ty -> Ty
NotI p = Imp p Bot

data Term : List Ty -> Ty -> Type where
  Var : Elem a g -> Term g a
  Lam : Term (a::g) b -> Term g (Imp a b)
  App : Term g (Imp a b) -> Term g a -> Term g b
  TT  : Term g Top
  Lob : Term [] (Imp (Box a) a) -> Term [] a

BoxO : Ty -> Type
BoxO = Term []

mutual
  intCtx : List Ty -> Type
  intCtx []     = ()
  intCtx (a::g) = (intTy a, intCtx g)

  intTy : Ty -> Type
  intTy (Imp a b) = intTy a -> intTy b
  intTy  Top      = ()
  intTy  Bot      = Void
  intTy (Box a)   = BoxO a

intTm: Term g t -> intCtx g -> intTy t
intTm (Var Here)       (ia, _) = ia
intTm (Var (There el)) (_, ig) = assert_total $ intTm (Var el) ig
intTm (Lam f)           ig     = \a => intTm f (a, ig)
intTm (App f a)         ig     = (intTm f ig) (intTm a ig)
intTm TT                ig     = ()
intTm (Lob t)           ()     = (intTm t ()) (Lob t)

consistent : Not (BoxO Bot)
consistent t = intTm t ()

incomplete0 : BoxO (NotI (Box Bot)) -> BoxO Bot
incomplete0 = Lob

-- Goedel's 2nd theorem
incomplete : Not (BoxO (NotI (Box Bot)))
incomplete = consistent . incomplete0