not-trouble.agda

module Scratch where

infixr 60 _*_
infixr 50 _=>_

data Ty : Set where
  Zero One : Ty
  _*_ _=>_ : Ty → Ty → Ty

infixl 40 _,_

data Ctx : Set where
  <> : Ctx
  _,_ : Ctx → Ty → Ctx

data Var : Ctx → Ty → Set where
  here : ∀ {G A} → Var (G , A) A
  there : ∀ {G A B} → Var G A → Var (G , B) A

infixl 30 _$_

data Tm (G : Ctx) : Ty → Set where
  var   : ∀ {A} → Var G A → Tm G A
  unit  : Tm G One
  abort : ∀ {C}   →   Tm G Zero   →   Tm G C
  <_,_> : ∀ {A B} →   Tm G A   →   Tm G B   →   Tm G (A * B)
  fst   : ∀ {A B} →   Tm G (A * B)   →   Tm G A
  snd   : ∀ {A B} →   Tm G (A * B)   →   Tm G B
  lam   : ∀ {A B} →   Tm (G , A) B   →   Tm G (A => B)
  _$_   : ∀ {A B} →   Tm G (A => B)   →   Tm G A → Tm G B

infix 20 _!-_::_

data _!-_::_ (G : Ctx) : (A : Ty) → Tm G A → Set where
  meta-var   : ∀ {A}   →   (x : Var G A)   →   G !- A :: var x
  meta-unit  : G !- One :: unit
  meta-abort : ∀ {C M}     →   G !- Zero :: M   →   G !- C :: abort M
  meta-pair  : ∀ {A B M N} →   G !- A :: M   →   G !- B :: N   →   G !- A * B :: < M , N >
  meta-fst   : ∀ {A B M}   →   G !- A * B :: M   →   G !- A :: fst M
  meta-snd   : ∀ {A B M}   →   G !- A * B :: M   →   G !- B :: snd M
  meta-lam   : ∀ {A B M}   →   G , A !- B :: M   →   G !- A => B :: lam M
  meta-app   : ∀ {A B M N} →   G !- A => B :: M   →   G !- A :: N   →   G !- B :: M $ N

infix 10 _!-_::_:::_

data _!-_::_:::_ (G : Ctx) : (A : Ty) → (M : Tm G A) → G !- A :: M → Set where
  meta-meta-var   : ∀ {A} →   (x : Var G A)   →   (v : G !- A :: var x)   →   G !- A :: var x ::: meta-var x
  meta-meta-unit  : G !- One :: unit ::: meta-unit
  meta-meta-abort : ∀ {C M MetaM}           →   G !- Zero :: M ::: MetaM   →   G !- C :: abort M ::: meta-abort MetaM
  meta-meta-pair  : ∀ {A B M N MetaM MetaN} →   G !- A :: M ::: MetaM   →   G !- B :: N ::: MetaN   →   G !- A * B :: < M , N > ::: meta-pair MetaM MetaN
  meta-meta-fst   : ∀ {A B M MetaM}         →   G !- A * B :: M ::: MetaM   →   G !- A :: fst M ::: meta-fst MetaM
  meta-meta-snd   : ∀ {A B M MetaM}         →   G !- A * B :: M ::: MetaM   →   G !- B :: snd M ::: meta-snd MetaM
  meta-meta-lam   : ∀ {A B M MetaM}         →   G , A !- B :: M ::: MetaM   →   G !- A => B :: lam M ::: meta-lam MetaM
  meta-meta-app   : ∀ {A B M N MetaM MetaN} →   G !- A => B :: M ::: MetaM   →   G !- A :: N ::: MetaN   →   G !- B :: M $ N ::: meta-app MetaM MetaN