Prove transfer.

3 files changed, 179 insertions, 25 deletions

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index 6b7a9dc..1a37aa0 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -11,40 +11,43 @@ open import Data.Empty
 open import Data.Fin as F hiding (cast)
 open import Data.Fin.Properties hiding (≤-trans)
 open import Data.Nat as ℕ hiding (_⊔_)
-open import Data.Nat.Properties
+open import Data.Nat.Properties as NP
 open import Data.Product
 open import Data.Vec
 open import Level renaming (suc to lsuc)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 
+≤-recomputable : ∀ {m n} → .(m ℕ.≤ n) → m ℕ.≤ n
+≤-recomputable {ℕ.zero} {n} m≤n = z≤n
+≤-recomputable {suc m} {suc n} m≤n = s≤s (≤-recomputable (pred-mono m≤n))
+
 cast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec {a} A n
 cast {m = 0} {0} eq [] = []
 cast {m = suc _} {suc n} eq (x ∷ xs) = x ∷ cast (cong ℕ.pred eq) xs
 
-reduce≥′ : ∀ {m n} → .(m ℕ.≤ n) → (i : Fin n) → toℕ i ≥ m → Fin (n ∸ m)
+reduce≥′ : ∀ {m n} → .(m ℕ.≤ n) → (i : Fin n) → .(_ : toℕ i ≥ m) → Fin (n ∸ m)
 reduce≥′ {ℕ.zero} {n} m≤n i i≥m = i
-reduce≥′ {suc m} {suc n} m≤n (suc i) (s≤s i≥m) = reduce≥′ (pred-mono m≤n) i i≥m
-
-private
-  insert′ : ∀ {a A m n} → Vec {a} A (n ∸ m) → m ℕ.≤ n → m ≢ 0 → (i : Fin (n ∸ ℕ.pred m)) → A → Vec A (n ∸ ℕ.pred m)
-  insert′ {a} {A} {ℕ.zero} {n} xs m≤n m≢0 i x = ⊥-elim (m≢0 refl)
-  insert′ {a} {A} {suc ℕ.zero} {suc _} xs _ _ F.zero x = x ∷ xs
-  insert′ {a} {A} {suc ℕ.zero} {suc (suc n)} (y ∷ xs) _ _ (suc i) x = y ∷ insert′ {m = suc ℕ.zero} {suc n} xs (s≤s z≤n) (λ ()) i x
-  insert′ {a} {A} {suc (suc m)} {suc ℕ.zero} xs m≤n _ i x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) m≤n)
-  insert′ {a} {A} {suc (suc m)} {suc (suc n)} xs m≤n _ i x = insert′ {m = suc m} xs (pred-mono m≤n) (λ ()) i x
-
-  reduce≥′-mono : ∀ {m n} → .(m≤n : m ℕ.≤ n) → (i j : Fin n) → (i≥m : toℕ i ≥ m) → (i≤j : i F.≤ j) → reduce≥′ m≤n i i≥m F.≤ reduce≥′ m≤n j (≤-trans i≥m i≤j)
-  reduce≥′-mono {ℕ.zero} {n} m≤n i j i≥m i≤j = i≤j
-  reduce≥′-mono {suc m} {suc n} m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = reduce≥′-mono (pred-mono m≤n) i j i≥m i≤j
-
-  remove′ : ∀ {a A m} → Vec {a} A m → .(m ≢ 0) → Fin m → Vec A (ℕ.pred m)
-  remove′ (x ∷ xs) m≢0 F.zero = xs
-  remove′ (x ∷ y ∷ xs) m≢0 (suc i) = x ∷ remove′ (y ∷ xs) (λ ()) i
-
-  rotate : ∀ {a A n} → (i j : Fin n) → .(i F.≤ j) → Vec {a} A n → Vec A n
-  rotate F.zero j i≤j (x ∷ xs) = insert xs j x
-  rotate (suc i) (suc j) i≤j (x ∷ xs) = x ∷ (rotate i j (pred-mono i≤j) xs)
+reduce≥′ {suc m} {suc n} m≤n (suc i) i≥m = reduce≥′ (pred-mono m≤n) i (pred-mono i≥m)
+
+reduce≥′-mono : ∀ {m n} → .(m≤n : m ℕ.≤ n) → (i j : Fin n) → (i≥m : toℕ i ≥ m) → (i≤j : i F.≤ j) → reduce≥′ m≤n i i≥m F.≤ reduce≥′ m≤n j (≤-trans i≥m i≤j)
+reduce≥′-mono {ℕ.zero} {n} m≤n i j i≥m i≤j = i≤j
+reduce≥′-mono {suc m} {suc n} m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = reduce≥′-mono (pred-mono m≤n) i j i≥m i≤j
+
+insert′ : ∀ {a A m n} → Vec {a} A (n ∸ m) → .(m ℕ.≤ n) → m ≢ 0 → (i : Fin (n ∸ ℕ.pred m)) → A → Vec A (n ∸ ℕ.pred m)
+insert′ {a} {A} {ℕ.zero} xs m≤n m≢0 i x = ⊥-elim (m≢0 refl)
+insert′ {a} {A} {suc ℕ.zero} xs _ _ F.zero x = x ∷ xs
+insert′ {a} {A} {suc ℕ.zero} (y ∷ xs) _ _ (suc i) x = y ∷ insert′ xs (s≤s z≤n) (λ ()) i x
+insert′ {a} {A} {suc (suc m)} {suc ℕ.zero} xs m≤n _ i x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable m≤n))
+insert′ {a} {A} {suc (suc m)} {suc (suc _)} xs m≤n _ i x = insert′ {m = suc m} xs (pred-mono m≤n) (λ ()) i x
+
+rotate : ∀ {a A n} → (i j : Fin n) → .(i F.≤ j) → Vec {a} A n → Vec A n
+rotate F.zero j i≤j (x ∷ xs) = insert xs j x
+rotate (suc i) (suc j) i≤j (x ∷ xs) = x ∷ (rotate i j (pred-mono i≤j) xs)
+
+remove′ : ∀ {a A m} → Vec {a} A m → .(m ≢ 0) → Fin m → Vec A (ℕ.pred m)
+remove′ (x ∷ xs) m≢0 F.zero = xs
+remove′ (x ∷ y ∷ xs) m≢0 (suc i) = x ∷ remove′ (y ∷ xs) (λ ()) i
 
 record Context n : Set (c ⊔ lsuc ℓ) where
   field
diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda
index 2761fae..230c18b 100644
--- a/src/Cfe/Context/Properties.agda
+++ b/src/Cfe/Context/Properties.agda
@@ -8,6 +8,7 @@ module Cfe.Context.Properties
 
 open import Cfe.Context.Base over as C
 open import Cfe.Type over
+open import Data.Empty
 open import Data.Fin as F
 open import Data.Nat as ℕ
 open import Data.Nat.Properties
@@ -23,6 +24,11 @@ cast-involutive : ∀ {a A k m n} .(k≡m : k ≡ m) .(m≡n : m ≡ n) .(k≡n
 cast-involutive {k = zero} {zero} {zero} k≡m m≡n k≡n [] = refl
 cast-involutive {k = suc _} {suc _} {suc _} k≡m m≡n k≡n (x ∷ xs) = cong (x ∷_) (cast-involutive (cong ℕ.pred k≡m) (cong ℕ.pred m≡n) (cong ℕ.pred k≡n) xs)
 
+cast-insert : ∀ {a A m n} xs .(m≡n : _) i j .(_ : toℕ i ≡ toℕ j) y → C.cast {a} {A} {suc m} {suc n} (cong suc m≡n) (insert xs i y) ≡ insert (C.cast m≡n xs) j y
+cast-insert [] m≡n zero zero _ y = refl
+cast-insert (x ∷ xs) m≡n zero zero _ y = refl
+cast-insert {m = suc _} {n = suc _} (x ∷ xs) m≡n (suc i) (suc j) i≡j y = cong (x ∷_) (cast-insert xs (cong ℕ.pred m≡n) i j (cong ℕ.pred i≡j) y)
+
 wkn₁-shift : ∀ {n} (Γ,Δ : Context n) i i≥m τ → shift (wkn₁ Γ,Δ i i≥m τ) ≋ wkn₁ (shift Γ,Δ) i z≤n τ
 wkn₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i i≥m τ =
   refl ,
@@ -62,3 +68,54 @@ wkn₂-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i i≤m τ =
                                (trans (sym (+-∸-assoc m (pred-mono m≤n))) (m+n∸m≡n m n))
                                (xs ++ ys)))
   eq {m = suc m} {suc n} (x ∷ xs) ys m≤n (suc i) (s≤s i≤m) y = cong (x ∷_) (eq xs ys (pred-mono m≤n) i i≤m y)
+
+rotate₁-shift : ∀ {n} (Γ,Δ : Context n) i j i≥m i≤j → rotate₁ (shift Γ,Δ) i j z≤n i≤j ≋ shift (rotate₁ Γ,Δ i j i≥m i≤j)
+rotate₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i≥m i≤j =
+  refl ,
+  eq Γ Δ m≤n i j i≥m i≤j ,
+  refl
+  where
+  eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i j i≥m i≤j →
+    rotate {a} {A} i j i≤j (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ xs)) ≡
+    C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ rotate (reduce≥′ m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) xs)
+  eq {m = zero} {suc _} (x ∷ xs) [] _ zero j _ _ = sym (cast-insert xs refl j j refl x)
+  eq {m = zero} (x ∷ xs) [] _ (suc i) (suc j) _ i≤j = cong (x ∷_) (eq xs [] z≤n i j z≤n (pred-mono i≤j))
+  eq {m = suc _} {suc _} xs (y ∷ ys) m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = cong (y ∷_) (eq xs ys (pred-mono m≤n) i j i≥m i≤j)
+
+transfer-cons : ∀ {n} (Γ,Δ : Context n) i j i<m 1+j≥m τ → transfer (cons Γ,Δ τ) (suc i) (suc j) (s≤s i<m) (s≤s 1+j≥m) ≋ cons (transfer Γ,Δ i j i<m 1+j≥m) τ
+transfer-cons record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m τ =
+  refl , eq₁ Γ Δ m≤n (fromℕ< i<m) j 1+j≥m τ , eq₂ Δ (fromℕ< i<m) τ
+  where
+  eq₁ : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) (i : Fin (suc m)) j .(1+j≥m : _) y →
+    insert′ {a} {A} xs (s≤s m≤n) (λ ()) (reduce≥′ (≤-step m≤n) (suc j) 1+j≥m) (lookup (y ∷ ys) (suc i)) ≡
+    insert′ xs m≤n (λ ()) (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) (lookup ys i)
+  eq₁ {m = zero} {suc _} xs ys m≤n i j 1+j≥m y = refl
+  eq₁ {m = suc m} xs ys m≤n i zero 1+j≥m x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
+  eq₁ {m = suc m} {suc _} xs (x ∷ ys) m≤n i (suc j) 1+j≥m y = refl
+
+  eq₂ : ∀ {a A m} ys (i : Fin (suc m)) y →
+    remove′ {a} {A} (y ∷ ys) (λ ()) (suc i) ≡ y ∷ remove′ ys (λ ()) i
+  eq₂ (x ∷ ys) i y = refl
+
+transfer-shift : ∀ {n} (Γ,Δ : Context n) i j i<m 1+j≥m → rotate₁ (shift Γ,Δ) i j z≤n (pred-mono (≤-trans i<m 1+j≥m)) ≋ shift (transfer Γ,Δ i j i<m 1+j≥m)
+transfer-shift record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m =
+  refl ,
+  eq Γ Δ m≤n i j i<m 1+j≥m ,
+  refl
+  where
+  eq : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) i j i<m .(1+j≥m : _) →
+    rotate {a} {A} i j
+      (pred-mono {_} {suc (toℕ j)} (≤-trans i<m 1+j≥m))
+      (C.cast (trans (sym (+-∸-assoc (suc m) m≤n)) (m+n∸m≡n (suc m) n)) (ys ++ xs)) ≡
+    C.cast
+      (trans (sym (+-∸-assoc m (pred-mono (≤-step m≤n)))) (m+n∸m≡n (suc m) n))
+      ( remove′ ys (λ ()) (fromℕ< i<m) ++
+        insert′ xs m≤n (λ ())
+          (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m))
+          (lookup ys (fromℕ< i<m)))
+  eq {m = zero} {suc _} xs (y ∷ []) m≤n zero zero i<m 1+j≥m = refl
+  eq {m = zero} {suc (suc _)} (x ∷ xs) (y ∷ []) _ zero (suc j) _ _ = cong (x ∷_) (eq xs (y ∷ []) (s≤s z≤n) zero j (s≤s z≤n) (s≤s z≤n))
+  eq {m = zero} {suc _} _ (_ ∷ []) _ (suc _) _ (s≤s ()) _
+  eq {m = suc _} {suc _} _ (_ ∷ _) _ _ zero _ 1+j≥m = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
+  eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n zero (suc j) i<m 1+j≥m = cong (y ∷_) (eq xs (x ∷ ys) (pred-mono m≤n) zero j (s≤s z≤n) (pred-mono 1+j≥m))
+  eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n (suc i) (suc j) (s≤s i<m) 1+j≥m = cong (x ∷_) (eq xs (y ∷ ys) (pred-mono m≤n) i j i<m (pred-mono 1+j≥m))
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index 7f357f0..053ab73 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -6,15 +6,28 @@ module Cfe.Judgement.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open import Cfe.Context over renaming (wkn₁ to cwkn₁; wkn₂ to cwkn₂; _≋_ to _≋ᶜ_)
+open import Cfe.Context over
+  renaming
+  ( wkn₁ to cwkn₁
+  ; wkn₂ to cwkn₂
+  ; rotate to crotate
+  ; rotate₁ to crotate₁
+  ; transfer to ctransfer
+  ; _≋_ to _≋ᶜ_
+  )
 open import Cfe.Expression over
 open import Cfe.Judgement.Base over
-open import Data.Fin
+open import Data.Empty
+open import Data.Fin as F
+open import Data.Fin.Properties hiding (≤-refl; ≤-trans; ≤-irrelevant)
 open import Data.Nat as ℕ
 open import Data.Nat.Properties
 open import Data.Product
 open import Data.Vec
+open import Data.Vec.Properties
+open import Function
 open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
 
 toℕ-punchIn : ∀ {n} i j → toℕ j ℕ.≤ toℕ (punchIn {n} i j)
 toℕ-punchIn zero j = n≤1+n (toℕ j)
@@ -65,3 +78,84 @@ wkn₂ {Γ,Δ = Γ,Δ} (Var {i = j} j≥m) i τ′ i≤m =
 wkn₂ (Fix Γ,Δ⊢e∶τ) i τ′ i≤m = Fix (wkn₂ Γ,Δ⊢e∶τ (suc i) τ′ (s≤s i≤m))
 wkn₂ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i τ′ i≤m = Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ i τ′ i≤m) (congᶜ (≋-sym (wkn₂-shift Γ,Δ i i≤m τ′)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ i τ′ z≤n)) τ₁⊛τ₂
 wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i τ′ i≤m = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ i τ′ i≤m) (wkn₂ Γ,Δ⊢e₂∶τ₂ i τ′ i≤m) τ₁#τ₂
+
+rotate₁ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i j i≥m i≤j → crotate₁ Γ,Δ i j i≥m i≤j ⊢ rotate e i j i≤j ∶ τ
+rotate₁ Eps i j i≥m i≤j = Eps
+rotate₁ (Char c) i j i≥m i≤j = Char c
+rotate₁ Bot i j i≥m i≤j = Bot
+rotate₁ {suc n} {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = k} k≥m) i j i≥m i≤j with i F.≟ k
+... | yes refl = congᵗ (τ≡τ′ Γ m≤n i j i≥m i≤j) (Var (≤-trans i≥m i≤j))
+  where
+    τ≡τ′ : ∀ {a A m n} xs m≤n i j i≥m i≤j → lookup {a} {A} (crotate (reduce≥′ {m} {n} m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) xs) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) ≡ lookup xs (reduce≥′ m≤n i i≥m)
+    τ≡τ′ {m = zero} (x ∷ xs) m≤n zero j i≥m i≤j = insert-lookup xs j x
+    τ≡τ′ {m = zero} (x ∷ xs) m≤n (suc i) (suc j) i≥m i≤j = τ≡τ′ xs z≤n i j z≤n (pred-mono i≤j)
+    τ≡τ′ {m = suc m} {suc n} xs m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = τ≡τ′ xs (pred-mono m≤n) i j i≥m i≤j
+... | no i≢k = congᵗ (τ≡τ′ Γ m≤n i j k i≢k i≥m i≤j k≥m) (Var (punchIn-punchOut≥m i j k i≢k i≥m i≤j k≥m))
+  where
+  punchIn-punchOut≥m : ∀ {m n} (i j k : Fin (suc n)) (i≢k : i ≢ k) → toℕ i ≥ m → i F.≤ j → toℕ k ≥ m → toℕ (punchIn j (punchOut i≢k)) ≥ m
+  punchIn-punchOut≥m {zero} _ _ _ _ _ _ _ = z≤n
+  punchIn-punchOut≥m {suc _} zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl)
+  punchIn-punchOut≥m {suc _} zero zero (suc _) _ _ _ k≥m = k≥m
+  punchIn-punchOut≥m {suc _} {suc _} (suc i) (suc j) (suc k) i≢k (s≤s i≥m) (s≤s i≤j) (s≤s k≥m) = s≤s (punchIn-punchOut≥m i j k (i≢k ∘ cong suc) i≥m i≤j k≥m)
+
+  τ≡τ′ : ∀ {a A m n} xs m≤n i j k i≢k i≥m i≤j k≥m →
+    lookup {a} {A}
+      (crotate
+        (reduce≥′ {m} {suc n} m≤n i i≥m)
+        (reduce≥′ m≤n j (≤-trans i≥m i≤j))
+        (reduce≥′-mono m≤n i j i≥m i≤j) xs)
+        (reduce≥′
+          m≤n
+          (punchIn j (punchOut i≢k))
+          (punchIn-punchOut≥m i j k i≢k i≥m i≤j k≥m)) ≡
+    lookup xs (reduce≥′ m≤n k k≥m)
+  τ≡τ′ {m = zero} _ _ zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl)
+  τ≡τ′ {m = zero} (_ ∷ _) _ zero zero (suc _) _ _ _ _ = refl
+  τ≡τ′ {m = zero} (_ ∷ _ ∷ _) _ zero (suc _) (suc zero) _ _ _ _ = refl
+  τ≡τ′ {m = zero} (x ∷ _ ∷ xs) _ zero (suc j) (suc (suc k)) _ _ _ _ = τ≡τ′ (x ∷ xs) z≤n zero j (suc k) (λ ()) z≤n z≤n z≤n
+  τ≡τ′ {m = zero} (_ ∷ _ ∷ _) _ (suc _) (suc _) zero _ _ _ _ = refl
+  τ≡τ′ {m = zero} (_ ∷ x ∷ xs) _ (suc i) (suc j) (suc k) i≢k _ i≤j _ = τ≡τ′ (x ∷ xs) z≤n i j k (i≢k ∘ cong suc) z≤n (pred-mono i≤j) z≤n
+  τ≡τ′ {m = suc m} {suc _} xs m≤n (suc i) (suc j) (suc k) i≢k i≥m i≤j k≥m = τ≡τ′ xs (pred-mono m≤n) i j k (i≢k ∘ cong suc) (pred-mono i≥m) (pred-mono i≤j) (pred-mono k≥m)
+rotate₁ (Fix Γ,Δ⊢e∶τ) i j i≥m i≤j = Fix (rotate₁ Γ,Δ⊢e∶τ (suc i) (suc j) (s≤s i≥m) (s≤s i≤j))
+rotate₁ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i j i≥m i≤j = Cat (rotate₁ Γ,Δ⊢e₁∶τ₁ i j i≥m i≤j) (congᶜ (rotate₁-shift Γ,Δ i j i≥m i≤j) (rotate₁ Δ++Γ,∙⊢e₂∶τ₂ i j z≤n i≤j)) τ₁⊛τ₂
+rotate₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i j i≥m i≤j = Vee (rotate₁ Γ,Δ⊢e₁∶τ₁ i j i≥m i≤j) (rotate₁ Γ,Δ⊢e₂∶τ₂ i j i≥m i≤j) τ₁#τ₂
+
+transfer : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i j i<m 1+j≥m → ctransfer Γ,Δ i j i<m 1+j≥m ⊢ rotate e i j (pred-mono (≤-trans i<m 1+j≥m)) ∶ τ
+transfer Eps i j i<m 1+j≥m = Eps
+transfer (Char c) i j i<m 1+j≥m = Char c
+transfer Bot i j i<m 1+j≥m = Bot
+transfer {suc n} {Γ,Δ = record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = k} k≥m) i j i<m 1+j≥m with suc m ℕ.≟ 0 | i F.≟ k
+... | no m≢0 | yes refl = ⊥-elim (<⇒≱ i<m k≥m)
+... | no m≢0 | no i≢k = congᵗ (τ≡τ′ Γ (lookup Δ (fromℕ< i<m)) m≢0 m≤n i j k i<m 1+j≥m k≥m i≢k) (Var (punchIn≥m i j k i≢k i<m 1+j≥m k≥m))
+  where
+  punchIn≥m : ∀ {m n} (i j k : Fin (suc n)) (i≢k : i ≢ k) → toℕ i ℕ.< m → .(suc (toℕ j) ≥ m) → toℕ k ≥ m → toℕ (punchIn j (punchOut i≢k)) ≥ ℕ.pred m
+  punchIn≥m {suc zero} _ _ _ _ _ _ _ = z≤n
+  punchIn≥m {suc (suc _)} zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl)
+  punchIn≥m {suc (suc _)} zero zero (suc _) _ _ _ (s≤s k≥m) = ≤-step k≥m
+  punchIn≥m {suc (suc _)} {suc _} (suc i) zero (suc k) i≢k (s≤s i<m) 1+j≥m (s≤s k≥m) = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
+  punchIn≥m {suc (suc _)} zero (suc _) (suc zero) _ _ _ (s≤s k≥m) = k≥m
+  punchIn≥m {suc (suc _)} zero (suc j) (suc (suc k)) _ _ 1+j≥m (s≤s k≥m) = s≤s (punchIn≥m zero j (suc k) (λ ()) (s≤s z≤n) (pred-mono 1+j≥m) k≥m)
+  punchIn≥m {suc (suc _)} {suc _} (suc i) (suc j) (suc k) i≢k (s≤s i<m) 1+j≥m (s≤s k≥m) = s≤s (punchIn≥m i j k (i≢k ∘ cong suc) i<m (pred-mono 1+j≥m) k≥m)
+
+  τ≡τ′ : ∀ {a A m n} xs y m≢0 .(m≤n : _) i j k i<m .(1+j≥m : _) k≥m i≢k →
+    lookup
+      (insert′ {a} {A} {m} {suc n} xs m≤n m≢0
+        (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m))
+        y)
+      (reduce≥′
+        (pred-mono (≤-step m≤n))
+        (punchIn j (punchOut i≢k))
+        (punchIn≥m i j k i≢k i<m 1+j≥m k≥m)) ≡
+    lookup xs (reduce≥′ m≤n k k≥m)
+  τ≡τ′ {m = suc zero} _ _ _ _ zero zero (suc _) _ _ (s≤s z≤n) _ = refl
+  τ≡τ′ {m = suc zero} _ _ _ _ (suc _) zero (suc _) (s≤s ()) _ _ _
+  τ≡τ′ {m = suc zero} (_ ∷ _) _ _ _ zero (suc _) (suc zero) _ _ (s≤s z≤n) _ = refl
+  τ≡τ′ {m = suc zero} (_ ∷ xs) y _ _ zero (suc j) (suc (suc k)) _ _ (s≤s z≤n) _ = τ≡τ′ xs y (λ ()) (s≤s (z≤n)) zero j (suc k) (s≤s z≤n) (s≤s z≤n) (s≤s z≤n) (λ ())
+  τ≡τ′ {m = suc (suc _)} _ _ _ _ _ zero _ _ 1+j≥m _ _ = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
+  τ≡τ′ {m = suc (suc _)} _ _ _ _ zero _ (suc zero) _ _ (s≤s ()) _
+  τ≡τ′ {m = suc (suc _)} {suc (suc _)} xs y _ m≤n zero (suc j) (suc (suc k)) _ 1+j≥m (s≤s k≥m) _ = τ≡τ′ xs y (λ ()) (pred-mono m≤n) zero j (suc k) (s≤s z≤n) (pred-mono 1+j≥m) k≥m (λ ())
+  τ≡τ′ {m = suc (suc m)} xs y m≢0 m≤n (suc i) (suc j) (suc zero) (s≤s i<m) 1+j≥m (s≤s k≥m) i≢k = τ≡τ′ xs y (λ ()) (pred-mono m≤n) i j zero i<m (pred-mono 1+j≥m) k≥m (i≢k ∘ cong suc)
+  τ≡τ′ {m = suc (suc m)} xs y m≢0 m≤n (suc i) (suc j) (suc (suc k)) (s≤s i<m) 1+j≥m (s≤s k≥m) i≢k = τ≡τ′ xs y (λ ()) (pred-mono m≤n) i j (suc k) i<m (pred-mono 1+j≥m) k≥m (i≢k ∘ cong suc)
+transfer {Γ,Δ = Γ,Δ} {τ = τ} (Fix Γ,Δ⊢e∶τ) i j i<m 1+j≥m = Fix (congᶜ (transfer-cons Γ,Δ i j i<m 1+j≥m τ) (transfer Γ,Δ⊢e∶τ (suc i) (suc j) (s≤s i<m) (s≤s 1+j≥m)))
+transfer {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i j i<m 1+j≥m = Cat (transfer Γ,Δ⊢e₁∶τ₁ i j i<m 1+j≥m) (congᶜ (transfer-shift Γ,Δ i j i<m 1+j≥m) (rotate₁ Δ++Γ,∙⊢e₂∶τ₂ i j z≤n (pred-mono (≤-trans i<m 1+j≥m)))) τ₁⊛τ₂
+transfer (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i j i<m 1+j≥m = Vee (transfer Γ,Δ⊢e₁∶τ₁ i j i<m 1+j≥m) (transfer Γ,Δ⊢e₂∶τ₂ i j i<m 1+j≥m) τ₁#τ₂