module Core.Term

import Core.Thinning

import public Data.Fin

-- Definition ------------------------------------------------------------------

public export
data Term : Nat -> Type where
  Var : Fin n -> Term n

  Set : Term n

  Pi : Term n -> Term (S n) -> Term n
  Abs : Term (S n) -> Term n
  App : Term n -> Term n -> Term n

%name Term t, u, v

-- Weakening -------------------------------------------------------------------

public export
wkn : Term m -> m `Thins` n -> Term n
wkn (Var i) thin = Var (wkn i thin)
wkn Set thin = Set
wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin)
wkn (Abs t) thin = Abs (wkn t $ keep thin)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)

export
wknHomo :
  (t : Term k) ->
  (thin1 : k `Thins` m) ->
  (thin2 : m `Thins` n) ->
  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
wknHomo (Var i) thin1 thin2 = cong Var (wknHomo i thin1 thin2)
wknHomo Set thin1 thin2 = Refl
wknHomo (Pi t u) thin1 thin2 =
  cong2 Pi
    (wknHomo t thin1 thin2)
    (trans
      (wknHomo u (keep thin1) (keep thin2))
      (cong (wkn u) $ compKeep thin2 thin1))
wknHomo (Abs t) thin1 thin2 =
  cong Abs
    (trans
      (wknHomo t (keep thin1) (keep thin2))
      (cong (wkn t) $ compKeep thin2 thin1))
wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)