module Core.Term import Core.Context import Core.Var import Core.Thinning import Syntax.PreorderReasoning -- Definition ------------------------------------------------------------------ public export data Term : Context -> Type where Var : Var sx -> Term sx Set : Term sx Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx Abs : (n : Name) -> Term (sx :< n) -> Term sx App : Term sx -> Term sx -> Term sx %name Term t, u, v -- Weakening ------------------------------------------------------------------- public export wkn : Term sx -> sx `Thins` sy -> Term sy wkn (Var i) thin = Var $ wkn i thin wkn Set thin = Set wkn (Pi n t u) thin = Pi n (wkn t thin) (wkn u $ keep thin n) wkn (Abs n t) thin = Abs n (wkn t $ keep thin n) wkn (App t u) thin = App (wkn t thin) (wkn u thin) -- Is Homomorphic export wknHomo : (t : Term sx) -> (thin1 : sx `Thins` sy) -> (thin2 : sy `Thins` sz) -> 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 n t u) thin1 thin2 = cong2 (Pi n) (wknHomo t thin1 thin2) $ Calc $ |~ wkn (wkn u (keep thin1 n)) (keep thin2 n) ~~ wkn u (keep thin2 n . keep thin1 n) ...(wknHomo u (keep thin1 n) (keep thin2 n)) ~~ wkn u (keep (thin2 . thin1) n) ...(cong (wkn u) $ compKeep thin2 thin1 n) wknHomo (Abs n t) thin1 thin2 = cong (Abs n) $ Calc $ |~ wkn (wkn t (keep thin1 n)) (keep thin2 n) ~~ wkn t (keep thin2 n . keep thin1 n) ...(wknHomo t (keep thin1 n) (keep thin2 n)) ~~ wkn t (keep (thin2 . thin1) n) ...(cong (wkn t) $ compKeep thin2 thin1 n) wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)