diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-16 18:01:33 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-16 18:01:33 +0100 |
| commit | af7c222cc3e487cd3ca8b5dd8749b7e258da7c7c (patch) | |
| tree | 995c3a9d7bc6965d2de56b8a4e1f3f10376e6e86 /src/Term.idr | |
| parent | 5adc1ae9357e42937a601aab57d16b2190e10536 (diff) | |
Define semantics and encode types up to pairs.
Diffstat (limited to 'src/Term.idr')
| -rw-r--r-- | src/Term.idr | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/Term.idr b/src/Term.idr index e9f6b1f..bceecfe 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -74,12 +74,15 @@ namespace Smart export varCong : {0 i, j : Elem ty ctx} -> i = j -> Var i <~> Var j + varCong Refl = irrelevantEquiv reflexive export shiftVar : (i : Elem ty ctx) -> shift (Var i) <~> Var (There i) + shiftVar i = UpToThin (dropPoint i) export constCong : {0 t, u : Term ty' ctx} -> t <~> u -> Const t <~> Const u + constCong prf = mapCong Const prf export absCong : {0 t, u : Term ty' (ctx :< ty)} -> t <~> u -> Abs t <~> Abs u @@ -94,6 +97,7 @@ namespace Smart export sucCong : {0 t, u : Term N ctx} -> t <~> u -> Suc t <~> Suc u + sucCong prf = mapCong Suc prf export recCong : @@ -104,9 +108,6 @@ namespace Smart t2 <~> u2 -> t3 <~> u3 -> Rec t1 t2 t3 <~> Rec u1 u2 u3 - recCong prf1 prf2 prf3 = - mapCong Rec - ?recCong_rhs_1 -- Substitution Definition ----------------------------------------------------- @@ -333,9 +334,9 @@ substBase : (thin : ctx `Thins` ctx') -> subst t (Base thin) <~> wkn t thin -export -substHomo : - (t : Term ty ctx) -> - (sub1 : Subst ctx ctx') -> - (sub2 : Subst ctx' ctx'') -> - subst (subst t sub1) sub2 <~> subst t ?d +-- export +-- substHomo : +-- (t : Term ty ctx) -> +-- (sub1 : Subst ctx ctx') -> +-- (sub2 : Subst ctx' ctx'') -> +-- subst (subst t sub1) sub2 <~> subst t ?d |