diff options
| -rw-r--r-- | src/Core/Term.idr | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr index 182e1ea..7e1a91c 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -32,6 +32,26 @@ 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) +-- Respects Identity + +export +wknId : (t : Term sx) -> wkn t (id sx) = t +wknId (Var i) = cong Var (wknId i) +wknId Set = Refl +wknId (Pi n t u) = + cong2 (Pi n) (wknId t) $ + Calc $ + |~ wkn u (keep (id sx) n) + ~~ wkn u (id $ sx :< n) ...(cong (wkn u) $ keepIdIsId sx n) + ~~ u ...(wknId u) +wknId (Abs n t) = + cong (Abs n) $ + Calc $ + |~ wkn t (keep (id sx) n) + ~~ wkn t (id $ sx :< n) ...(cong (wkn t) $ keepIdIsId sx n) + ~~ t ...(wknId t) +wknId (App t u) = cong2 App (wknId t) (wknId u) + -- Is Homomorphic export |