1 files changed, 76 insertions, 1 deletions
diff --git a/src/Core/Var.idr b/src/Core/Var.idr
index 791151d..c211ce3 100644
--- a/src/Core/Var.idr
+++ b/src/Core/Var.idr
@@ -35,7 +35,7 @@ there (MakeVar index prf) = MakeVar (S index) (There prf)
 namespace View
   public export
   data View : Var sx -> Type where
-    Here : View Core.Var.here
+    Here : View (here {sx, n})
     There : (i : Var sx) -> View (there i)
 
   %name View.View view
@@ -87,6 +87,12 @@ export
 wkn : Var sx -> sx `Thins` sy -> Var sy
 wkn i thin = doWkn i (view thin)
 
+-- Respects Identity
+
+export
+wknId : (i : Var sx) -> wkn i (id sx) = i
+wknId i = cong (doWkn i) $ viewUnique (view (id sx)) (Id sx)
+
 -- Is Homomorphic
 
 export
@@ -161,3 +167,72 @@ wknHomo :
   (thin2 : sy `Thins` sz) ->
   wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
 wknHomo i thin1 thin2 = doWknHomo i (view thin1) (view thin2)
+
+-- Concrete weakenings
+
+export
+wknDropIsThere :
+  (i : Var sx) ->
+  (thin : sx `Thins` sy) ->
+  (0 n : Name) ->
+  wkn i (drop thin n) = there (wkn i thin)
+wknDropIsThere i thin n = rewrite viewUnique (view $ drop thin n) (Drop thin n) in Refl
+
+export
+wknKeepHereIsHere :
+  (thin : sx `Thins` sy) ->
+  (0 n : Name) ->
+  wkn Core.Var.here (keep thin n) = Core.Var.here
+wknKeepHereIsHere thin n = lemma $ view thin
+  where
+  lemma :
+    forall sx, sy.
+    {0 thin : sx `Thins` sy} ->
+    View thin ->
+    wkn Core.Var.here (keep thin n) = Core.Var.here
+  lemma (Id sx) =
+    rewrite keepIdIsId sx n in
+    rewrite viewUnique (view $ id $ sx :< n) (Id $ sx :< n) in
+    Refl
+  lemma (Drop thin m) =
+    rewrite viewUnique (view $ keep (drop thin m) n) (Keep {prf = dropIsNotId thin m} _ n) in
+    Refl
+  lemma (Keep {prf} thin m) =
+    rewrite
+      viewUnique
+        (view $ keep (keep thin m) n)
+        (Keep {prf = keepNotIdIsNotId prf m} (keep thin m) n)
+    in
+    Refl
+
+export
+wknKeepThereIsThere :
+  (i : Var sx) ->
+  (thin : sx `Thins` sy) ->
+  (0 n : Name) ->
+  wkn (there i) (keep thin n) = there (wkn i thin)
+wknKeepThereIsThere i thin n = lemma i $ view thin
+  where
+  lemma :
+    forall sx, sy.
+    (i : Var sx) ->
+    {0 thin : sx `Thins` sy} ->
+    View thin ->
+    wkn (there i) (keep thin n) = there (wkn i thin)
+  lemma i (Id sx) =
+    rewrite keepIdIsId sx n in
+    rewrite viewUnique (view $ id $ sx :< n) (Id $ sx :< n) in
+    rewrite viewUnique (view $ id sx) (Id sx) in
+    Refl
+  lemma i (Drop thin m) =
+    rewrite viewUnique (view $ keep (drop thin m) n) (Keep {prf = dropIsNotId thin m} _ n) in
+    rewrite viewUnique (view $ there {n} i) (There i) in
+    Refl
+  lemma i (Keep {prf} thin m) =
+    rewrite
+      viewUnique
+        (view $ keep (keep thin m) n)
+        (Keep {prf = keepNotIdIsNotId prf m} (keep thin m) n)
+    in
+    rewrite viewUnique (view $ there {n} i) (There i) in
+    Refl