diff options
Diffstat (limited to 'src/Core/Term/Thinned.idr')
| -rw-r--r-- | src/Core/Term/Thinned.idr | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr index 3a06612..6a6c0ff 100644 --- a/src/Core/Term/Thinned.idr +++ b/src/Core/Term/Thinned.idr @@ -49,9 +49,33 @@ wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $ ~~ wkn u (thin . thin2) ...(wknHomo u thin2 thin) export +wknId : (t : Thinned n) -> wkn t (id n) = t +wknId (t `Over` thin) = cong (t `Over`) (compLeftId thin) + +export wknHomo : (t : Thinned k) -> (thin1 : k `Thins` m) -> (thin2 : m `Thins` n) -> wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1) wknHomo (t `Over` thin) thin1 thin2 = cong (t `Over`) (compAssoc thin2 thin1 thin) + +export +wkn1Comm : + (t : Thinned m) -> + (thin : m `Thins` n) -> + wkn (wkn t thin) (wkn1 n) = wkn (wkn t $ wkn1 m) (keep thin) +wkn1Comm (t `Over` thin') thin = cong (t `Over`) $ Calc $ + |~ wkn1 n . (thin . thin') + ~~ drop (thin . thin') ...(compLeftWkn1 (thin . thin')) + ~~ keep thin . drop thin' ...(sym $ compRightDrop thin thin') + ~~ keep thin . (wkn1 m . thin') ...(sym $ cong (keep thin .) $ compLeftWkn1 thin') + +-- Interaction with Expansion + +export +expandHomo : + (t : Thinned m) -> + (thin : m `Thins` n) -> + expand (wkn t thin) = wkn (expand t) thin +expandHomo (t `Over` thin') thin = sym (wknHomo t thin' thin) |