diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 16:35:15 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 16:35:15 +0100 |
| commit | a38b0b5a6ee30e7dd22bc91765ba5361ed807dda (patch) | |
| tree | b2e4006c3d2feef19281aafb559f001bc3986693 /src/Core/Term.idr | |
| parent | 5f83999f483e241158706522a35364ba32f7f203 (diff) | |
Prove substitution respects the quotient.
Diffstat (limited to 'src/Core/Term.idr')
| -rw-r--r-- | src/Core/Term.idr | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr index 1b050ca..74ef7af 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -27,3 +27,24 @@ wkn Set thin = Set wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin) wkn (Abs t) thin = Abs (wkn t $ keep thin) wkn (App t u) thin = App (wkn t thin) (wkn u thin) + +export +wknHomo : + (t : Term k) -> + (thin1 : k `Thins` m) -> + (thin2 : m `Thins` n) -> + 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 t u) thin1 thin2 = + cong2 Pi + (wknHomo t thin1 thin2) + (trans + (wknHomo u (keep thin1) (keep thin2)) + (cong (wkn u) $ compKeep thin2 thin1)) +wknHomo (Abs t) thin1 thin2 = + cong Abs + (trans + (wknHomo t (keep thin1) (keep thin2)) + (cong (wkn t) $ compKeep thin2 thin1)) +wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) |