diff options
| -rw-r--r-- | src/Core/Term.idr | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr index 930e68f..28e229d 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -4,6 +4,8 @@ import Core.Context import Core.Var import Core.Thinning +import Syntax.PreorderReasoning + -- Definition ------------------------------------------------------------------ public export @@ -18,7 +20,7 @@ data Term : Context -> Type where %name Term t, u, v --- Operations ------------------------------------------------------------------ +-- Weakening ------------------------------------------------------------------- public export wkn : Term sx -> sx `Thins` sy -> Term sy @@ -27,3 +29,27 @@ 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) |