diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:25:29 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:25:29 +0100 |
| commit | 69d8b5c52f8685e3b6332b1fa9892d2f1060adc4 (patch) | |
| tree | 2a3f97f284280c9ffda6178cebe3c6493d6b0005 /src/Core/Term | |
| parent | b7a8063be92fb6c83de1ea60ac09c49f895886ff (diff) | |
Prove weakening a thinned term is homomorphic.
Diffstat (limited to 'src/Core/Term')
| -rw-r--r-- | src/Core/Term/Thinned.idr | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr index 3ed4779..3a06612 100644 --- a/src/Core/Term/Thinned.idr +++ b/src/Core/Term/Thinned.idr @@ -47,3 +47,11 @@ wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $ ~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin) ~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf) ~~ wkn u (thin . thin2) ...(wknHomo u thin2 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) |