Add weakening proofs for type judgements.

5 files changed, 277 insertions, 15 deletions

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index c4940b6..f4a8dc0 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -15,11 +15,12 @@ open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ₗ_)
 open import Cfe.Language.Construct.Single over
 open import Cfe.Language.Construct.Union over
 open import Cfe.Language.Indexed.Construct.Iterate over
-open import Data.Fin as F hiding (_≤_)
+open import Data.Fin as F hiding (_≤_; cast)
 open import Data.Nat as ℕ hiding (_≤_; _⊔_)
 open import Data.Product
 open import Data.Vec
 open import Level renaming (suc to lsuc) hiding (Lift)
+open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 
 infix 10 _[_/_]
@@ -36,6 +37,15 @@ data Expression : ℕ → Set c where
   Var : ∀ {n} → Fin n → Expression n
   μ : ∀ {n} → Expression (suc n) → Expression n
 
+cast : ∀ {m n} → .(_ : m ≡ n) → Expression m → Expression n
+cast eq ⊥ = ⊥
+cast eq ε = ε
+cast eq (Char x) = Char x
+cast eq (e₁ ∨ e₂) = cast eq e₁ ∨ cast eq e₂
+cast eq (e₁ ∙ e₂) = cast eq e₁ ∙ cast eq e₂
+cast eq (Var i) = Var (F.cast eq i)
+cast eq (μ e) = μ (cast (cong suc eq) e)
+
 wkn : ∀ {n} → Expression n → Fin (suc n) → Expression (suc n)
 wkn ⊥ i = ⊥
 wkn ε i = ε
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index e810ce4..1e41f42 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -9,12 +9,13 @@ module Cfe.Expression.Properties
 open Setoid over using () renaming (Carrier to C)
 
 open import Algebra
-open import Cfe.Expression.Base over
+open import Cfe.Expression.Base over as E
 open import Cfe.Language over as L
 import Cfe.Language.Construct.Concatenate over as ∙
 import Cfe.Language.Construct.Union over as ∪
 import Cfe.Language.Indexed.Construct.Iterate over as ⋃
 open import Data.Fin as F
+open import Data.Fin.Properties
 open import Data.Nat as ℕ hiding (_⊔_)
 open import Data.Product
 open import Data.Sum
@@ -190,10 +191,39 @@ subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin
   insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i
 
 monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
-monotone ⊥ γ≤γ′ = ≤-refl
-monotone ε γ≤γ′ = ≤-refl
-monotone (Char x) γ≤γ′ = ≤-refl
+monotone ⊥ γ≤γ′ = L.≤-refl
+monotone ε γ≤γ′ = L.≤-refl
+monotone (Char x) γ≤γ′ = L.≤-refl
 monotone (e₁ ∨ e₂) γ≤γ′ = ∪.∪-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
 monotone (e₁ ∙ e₂) γ≤γ′ = ∙.∙-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
 monotone (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
 monotone (μ e) γ≤γ′ = ⋃.⋃-monotone (λ x≤y → monotone e (x≤y PW.∷ γ≤γ′))
+
+cast-inverse : ∀ {m n} e → .(m≡n : m ≡ n) → .(n≡m : n ≡ m) → E.cast m≡n (E.cast n≡m e) ≡ e
+cast-inverse ⊥ m≡n n≡m = ≡.refl
+cast-inverse ε m≡n n≡m = ≡.refl
+cast-inverse (Char x) m≡n n≡m = ≡.refl
+cast-inverse (e₁ ∨ e₂) m≡n n≡m = ≡.cong₂ _∨_ (cast-inverse e₁ m≡n n≡m) (cast-inverse e₂ m≡n n≡m)
+cast-inverse (e₁ ∙ e₂) m≡n n≡m = ≡.cong₂ _∙_ (cast-inverse e₁ m≡n n≡m) (cast-inverse e₂ m≡n n≡m)
+cast-inverse (Var x) m≡n n≡m = ≡.cong Var (toℕ-injective (begin
+  toℕ (F.cast m≡n (F.cast n≡m x)) ≡⟨ toℕ-cast m≡n (F.cast n≡m x) ⟩
+  toℕ (F.cast n≡m x)              ≡⟨ toℕ-cast n≡m x ⟩
+  toℕ x                           ∎))
+  where
+  open ≡.≡-Reasoning
+cast-inverse (μ e) m≡n n≡m = ≡.cong μ (cast-inverse e (≡.cong suc m≡n) (≡.cong suc n≡m))
+
+cast-involutive : ∀ {k m n} e → .(k≡m : k ≡ m) → .(m≡n : m ≡ n) → .(k≡n : k ≡ n) → E.cast m≡n (E.cast k≡m e) ≡ E.cast k≡n e
+cast-involutive ⊥ k≡m m≡n k≡n = ≡.refl
+cast-involutive ε k≡m m≡n k≡n = ≡.refl
+cast-involutive (Char x) k≡m m≡n k≡n = ≡.refl
+cast-involutive (e₁ ∨ e₂) k≡m m≡n k≡n = ≡.cong₂ _∨_ (cast-involutive e₁ k≡m m≡n k≡n) (cast-involutive e₂ k≡m m≡n k≡n)
+cast-involutive (e₁ ∙ e₂) k≡m m≡n k≡n = ≡.cong₂ _∙_ (cast-involutive e₁ k≡m m≡n k≡n) (cast-involutive e₂ k≡m m≡n k≡n)
+cast-involutive (Var x) k≡m m≡n k≡n = ≡.cong Var (toℕ-injective (begin
+  toℕ (F.cast m≡n (F.cast k≡m x)) ≡⟨ toℕ-cast m≡n (F.cast k≡m x) ⟩
+  toℕ (F.cast k≡m x)              ≡⟨ toℕ-cast k≡m x ⟩
+  toℕ x                           ≡˘⟨ toℕ-cast k≡n x ⟩
+  toℕ (F.cast k≡n x)              ∎))
+  where
+  open ≡.≡-Reasoning
+cast-involutive (μ e) k≡m m≡n k≡n = ≡.cong μ (cast-involutive e (≡.cong suc k≡m) (≡.cong suc m≡n) (≡.cong suc k≡n))
diff --git a/src/Cfe/Judgement.agda b/src/Cfe/Judgement.agda
index a77cf92..370f734 100644
--- a/src/Cfe/Judgement.agda
+++ b/src/Cfe/Judgement.agda
@@ -7,3 +7,4 @@ module Cfe.Judgement
   where
 
 open import Cfe.Judgement.Base over public
+open import Cfe.Judgement.Properties over public
diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda
index 0db2d8f..8b3bf55 100644
--- a/src/Cfe/Judgement/Base.agda
+++ b/src/Cfe/Judgement/Base.agda
@@ -6,21 +6,83 @@ module Cfe.Judgement.Base
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open import Cfe.Expression over
+open import Cfe.Expression over as E
 open import Cfe.Type over renaming (_∙_ to _∙ₜ_; _∨_ to _∨ₜ_)
 open import Cfe.Type.Construct.Lift over
-open import Data.Fin
+open import Data.Fin as F
 open import Data.Nat as ℕ hiding (_⊔_)
 open import Data.Vec hiding (_⊛_)
 open import Level hiding (Lift) renaming (suc to lsuc)
+open import Relation.Binary.PropositionalEquality
 
 infix 2 _,_⊢_∶_
+infix 4 _≅_
 
-data _,_⊢_∶_ {m} {n} : Vec (Type ℓ ℓ) m → Vec (Type ℓ ℓ) n → Expression (n ℕ.+ m) → Type ℓ ℓ → Set (c ⊔ lsuc ℓ) where
-  Eps : ∀ {Γ Δ} → Γ , Δ ⊢ ε ∶ Lift ℓ ℓ τε
-  Char : ∀ {Γ Δ} c → Γ , Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ]
-  Bot : ∀ {Γ Δ} → Γ , Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥
-  Var : ∀ {Γ Δ i} i≥n → Γ , Δ ⊢ Var i ∶ lookup Γ (reduce≥ i i≥n)
-  Fix : ∀ {Γ Δ e τ} → Γ , τ ∷ Δ ⊢ e ∶ τ → Γ , Δ ⊢ μ e ∶ τ
-  Cat : ∀ {Γ Δ e e′ τ τ′} → Γ , Δ ⊢ e ∶ τ → Δ ++ Γ , [] ⊢ e′ ∶ τ′ → τ ⊛ τ′ → Γ , Δ ⊢ e ∙ e′ ∶ τ ∙ₜ τ′
-  Vee : ∀ {Γ Δ e e′ τ τ′} → Γ , Δ ⊢ e ∶ τ → Γ , Δ ⊢ e′ ∶ τ′ → τ # τ′ → Γ , Δ ⊢ e ∨ e′ ∶ τ ∨ₜ τ′
+data _,_⊢_∶_ : {m : ℕ} → {n : ℕ} → Vec (Type ℓ ℓ) m → Vec (Type ℓ ℓ) n → Expression (n ℕ.+ m) → Type ℓ ℓ → Set (c ⊔ lsuc ℓ) where
+  Eps : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} → Γ , Δ ⊢ ε ∶ Lift ℓ ℓ τε
+  Char : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} c → Γ , Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ]
+  Bot : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} → Γ , Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥
+  Var : ∀ {m n : ℕ} {Γ : Vec _ m} {Δ : Vec _ n} {i : Fin (n ℕ.+ m)} (i≥n : toℕ i ≥ n) → Γ , Δ ⊢ Var i ∶ lookup Γ (reduce≥ i i≥n)
+  Fix : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e τ} → Γ , τ ∷ Δ ⊢ e ∶ τ → Γ , Δ ⊢ μ e ∶ τ
+  Cat : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Δ ++ Γ , [] ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ , Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂
+  Vee : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Γ , Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ , Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂
+
+vcast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec A n
+vcast {n = suc n} eq (x ∷ xs) = x ∷ vcast (suc-injective eq) xs
+  where
+  open import Data.Nat.Properties using (suc-injective)
+vcast {n = ℕ.zero} eq [] = []
+
+data _≅_ {a A} : {m n : ℕ} → Vec {a} A m → Vec A n → Set a where
+  []≅[] : [] ≅ []
+  _∷_ : ∀ {m n x y} {xs : Vec _ m} {ys : Vec _ n} → (x≡y : x ≡ y) → xs ≅ ys → x ∷ xs ≅ y ∷ ys
+
+≅-refl : ∀ {a A m} {xs : Vec {a} A m} → xs ≅ xs
+≅-refl {xs = []} = []≅[]
+≅-refl {xs = x ∷ xs} = refl ∷ ≅-refl
+
+≅-reflexive : ∀ {a A m} {xs : Vec {a} A m} {ys} → xs ≡ ys → xs ≅ ys
+≅-reflexive refl = ≅-refl
+
+≅-length : ∀ {a A m n} {xs : Vec {a} A m} {ys : Vec _ n} → xs ≅ ys → m ≡ n
+≅-length []≅[] = refl
+≅-length (_ ∷ xs≅ys) = cong suc (≅-length xs≅ys)
+
+≅⇒≡ : ∀ {a A m n} {xs : Vec {a} A m} {ys : Vec _ n} → (xs≅ys : xs ≅ ys) → vcast (≅-length xs≅ys) xs ≡ ys
+≅⇒≡ []≅[] = refl
+≅⇒≡ (x≡y ∷ xs≅ys) = cong₂ _∷_ x≡y (≅⇒≡ xs≅ys)
+
+++ˡ : ∀ {a A m n k} {xs : Vec {a} A m} {ys : Vec _ n} (zs : Vec _ k) → xs ≅ ys → zs ++ xs ≅ zs ++ ys
+++ˡ [] xs≅ys = xs≅ys
+++ˡ (z ∷ zs) xs≅ys = refl ∷ ++ˡ zs xs≅ys
+
+cast₁ : ∀ {m₁ m₂ n} {Γ₁ : Vec _ m₁} {Γ₂ : Vec _ m₂} {Δ : Vec _ n} {e τ} → (eq : Γ₁ ≅ Γ₂) → Γ₁ , Δ ⊢ e ∶ τ → Γ₂ , Δ ⊢ E.cast (cong (n ℕ.+_) (≅-length eq)) e ∶ τ
+cast₁ eq Eps = Eps
+cast₁ eq (Char c) = Char c
+cast₁ eq Bot = Bot
+cast₁ {n = n} {Γ₁} {Δ = Δ} eq (Var {i = i} i≥n) =
+  subst₂ (_, Δ ⊢ E.cast (cong (n ℕ.+_) (≅-length eq)) (Var i) ∶_)
+         (≅⇒≡ eq)
+         (eq′ Γ₁ i≥n (≅-length eq))
+         (Var (ge (≅-length eq) i≥n))
+  where
+  open import Data.Empty using (⊥-elim)
+  open import Data.Fin.Properties using (toℕ<n; toℕ-cast; toℕ-injective)
+  open import Data.Nat.Properties using (<⇒≱; +-identityʳ; module ≤-Reasoning)
+
+  ge : ∀ {m₁ m₂ n i} → .(eq : m₁ ≡ m₂) → toℕ {n ℕ.+ m₁} i ≥ n → toℕ (F.cast (cong (n ℕ.+_) eq) i) ≥ n
+  ge {n = ℕ.zero} {i} _ _ = z≤n
+  ge {n = suc n} {suc i} eq (s≤s i≥n) = s≤s (ge eq i≥n)
+
+  eq′ : ∀ {a A m₁ m₂ n i} Γ i≥n → (eq : m₁ ≡ m₂) → lookup {a} {A} {m₂} (vcast eq Γ) (reduce≥ {n} (F.cast (cong (n ℕ.+_) eq) i) (ge eq i≥n)) ≡ lookup Γ (reduce≥ i i≥n)
+  eq′ {m₁ = ℕ.zero} {ℕ.zero} {n} {i} Γ i≥n _ = ⊥-elim (<⇒≱ (begin-strict
+    toℕ i <⟨ toℕ<n i ⟩
+    n ℕ.+ 0 ≡⟨ +-identityʳ n ⟩
+    n ∎) i≥n)
+    where
+    open ≤-Reasoning
+  eq′ {m₁ = suc m₁} {suc m₁} {ℕ.zero} {i} Γ i≥n refl = cong₂ lookup {vcast refl Γ} (≅⇒≡ ≅-refl) (toℕ-injective (toℕ-cast refl i))
+  eq′ {m₁ = suc m₁} {suc m₂} {suc n} {suc i} Γ (s≤s i≥n) eq = eq′ Γ i≥n eq
+cast₁ eq (Fix Γ₁,τ∷Δ⊢e∶τ) = Fix (cast₁ eq Γ₁,τ∷Δ⊢e∶τ)
+cast₁ {Δ = Δ} eq (Cat Γ₁,Δ⊢e₁∶τ₁ Δ++Γ₁,∙⊢e₂∶τ₂ τ₁⊛τ₂) = Cat (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ (++ˡ Δ eq) Δ++Γ₁,∙⊢e₂∶τ₂) τ₁⊛τ₂
+cast₁ eq (Vee Γ₁,Δ⊢e₁∶τ₁ Γ₁,Δ⊢e₂∶τ₂ τ₁#τ₂) = Vee (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ eq Γ₁,Δ⊢e₂∶τ₂) τ₁#τ₂
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
new file mode 100644
index 0000000..b5183eb
--- /dev/null
+++ b/src/Cfe/Judgement/Properties.agda
@@ -0,0 +1,159 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Cfe.Judgement.Properties
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open import Cfe.Expression over
+open import Cfe.Judgement.Base over
+open import Cfe.Type over
+open import Data.Empty
+open import Data.Fin as F hiding (cast)
+open import Data.Fin.Properties
+open import Data.Nat as ℕ
+open import Data.Nat.Properties
+open import Data.Vec
+open import Data.Vec.Properties
+open import Function
+open import Relation.Binary.PropositionalEquality
+
+wkn₁ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+       Γ , Δ ⊢ e ∶ τ →
+       ∀ τ′ i →
+       insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (wkn e (F.cast (+-suc n m) (raise n i))) ∶ τ
+wkn₁ Eps τ′ i = Eps
+wkn₁ (Char c) τ′ i = Char c
+wkn₁ Bot τ′ i = Bot
+wkn₁ {m} {n} {Γ} {Δ} {e} {τ} (Var {i = j} j≥n) τ′ i =
+  subst (insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (Var (punchIn (F.cast (+-suc n m) (raise n i)) j)) ∶_)
+        (eq Γ τ′ i j≥n)
+        (Var (le i j≥n))
+  where
+  toℕ-punchIn : ∀ {m} i j → toℕ j ℕ.≤ toℕ (punchIn {m} i j)
+  toℕ-punchIn zero j = n≤1+n (toℕ j)
+  toℕ-punchIn (suc i) zero = z≤n
+  toℕ-punchIn (suc i) (suc j) = s≤s (toℕ-punchIn i j)
+
+  le : ∀ {m n} i {j} → toℕ j ≥ n → toℕ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) ≥ n
+  le {m} {n} i {j} j≥n = begin
+    n ≤⟨ j≥n ⟩
+    toℕ j ≤⟨ toℕ-punchIn (F.cast (+-suc n m) (raise n i)) j ⟩
+    toℕ (punchIn (F.cast _ (raise n i)) j) ≡˘⟨ toℕ-cast (sym (+-suc n m)) (punchIn (F.cast _ (raise n i)) j) ⟩
+    toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∎
+    where
+    open ≤-Reasoning
+
+  lookup-cast : ∀ {a A n} l j → lookup {a} {A} {n} l (F.cast refl j) ≡ lookup l j
+  lookup-cast l zero = refl
+  lookup-cast (x ∷ l) (suc j) = lookup-cast l j
+
+  toℕ-reduce : ∀ {m n} i i≥m → toℕ (reduce≥ {m} {n} i i≥m) ≡ toℕ i ∸ m
+  toℕ-reduce {zero} i i≥m = refl
+  toℕ-reduce {suc m} (suc i) (s≤s i≥m) = toℕ-reduce i i≥m
+
+  punchIn-∸ : ∀ {m n} i {j} j≥n → toℕ (punchIn (F.cast (+-suc n m) (raise n i)) j) ∸ n ≡ toℕ (punchIn i (reduce≥ j j≥n))
+  punchIn-∸ {zero} {n} zero {j} j≥n = ⊥-elim (<⇒≱ (begin-strict
+    toℕ j ≡˘⟨ toℕ-cast (+-identityʳ n) j ⟩
+    toℕ (F.cast _ j) <⟨ toℕ<n (F.cast _ j) ⟩
+    n ∎) j≥n)
+    where
+    open ≤-Reasoning
+  punchIn-∸ {suc m} {zero} zero {j} z≤n = refl
+  punchIn-∸ {suc m} {suc n} zero {suc j} (s≤s j≥n) = punchIn-∸ zero j≥n
+  punchIn-∸ {suc m} {zero} (suc i) {zero} z≤n = refl
+  punchIn-∸ {suc m} {zero} (suc i) {suc j} z≤n = cong suc (punchIn-∸ i z≤n)
+  punchIn-∸ {suc m} {suc n} (suc i) {suc j} (s≤s j≥n) = punchIn-∸ (suc i) j≥n
+
+  missing-link : ∀ {m n} i {j} j≥n → reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i j≥n) ≡ punchIn i (reduce≥ j j≥n)
+  missing-link {n = n} i {j} j≥n = toℕ-injective (begin
+    toℕ (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ toℕ-reduce (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n) ⟩
+    toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∸ n ≡⟨ cong (_∸ n) (toℕ-cast _ (punchIn (F.cast _ (raise n i)) j)) ⟩
+    toℕ (punchIn (F.cast _ (raise n i)) j) ∸ n ≡⟨ punchIn-∸ i j≥n ⟩
+    toℕ (punchIn i (reduce≥ j j≥n)) ∎)
+    where
+    open ≡-Reasoning
+
+  eq : ∀ {a} {A : Set a} {m n} (Γ : Vec A m) τ′ i {j} j≥n → lookup (insert Γ i τ′) (reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i {j} j≥n)) ≡ lookup Γ (reduce≥ j j≥n)
+  eq {n = n} Γ τ′ i {j} j≥n = begin
+    lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ cong (lookup (insert Γ i τ′)) (missing-link i j≥n) ⟩
+    lookup (insert Γ i τ′) (punchIn i (reduce≥ j j≥n)) ≡⟨ insert-punchIn Γ i τ′ (reduce≥ j j≥n) ⟩
+    lookup Γ (reduce≥ j j≥n) ∎
+    where
+    open ≡-Reasoning
+
+wkn₁ (Fix Γ,τ∷Δ⊢e∶τ) τ′ i = Fix (wkn₁ Γ,τ∷Δ⊢e∶τ τ′ i)
+wkn₁{m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) τ′ i =
+  Cat (wkn₁ Γ,Δ⊢e₁∶τ₁  τ′ i)
+      (subst (λ x → Δ ++ insert Γ i τ′ , [] ⊢ x ∶ τ₂)
+             (begin
+               cast _ (cast _ (wkn e₂ (F.cast refl (raise zero (F.cast _ (raise n i)))))) ≡⟨⟩
+               cast _ (cast _ (wkn e₂ (F.cast refl (F.cast _ (raise n i))))) ≡⟨ cast-involutive (wkn e₂ (F.cast refl (F.cast _ (raise n i)))) refl (sym (+-suc n m)) (sym (+-suc n m)) ⟩
+               cast _ (wkn e₂ (F.cast refl (F.cast _ (raise n i)))) ≡⟨ cong (λ x → cast (sym (+-suc n m)) (wkn e₂ x)) (fcast-involutive (raise n i) (+-suc n m) refl (+-suc n m)) ⟩
+               cast _ (wkn e₂ (F.cast _ (raise n i))) ∎)
+             (cast₁ (eq Γ Δ τ′ i) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ τ′ (F.cast (+-suc n m) (raise n i)))))
+      τ₁⊛τ₂
+  where
+  open ≡-Reasoning
+  eq : ∀ {a A m n} Γ Δ τ′ i → insert (Δ ++ Γ) (F.cast (+-suc n m) (raise n i)) τ′ ≅ Δ ++ insert {a} {A} {m} Γ i τ′
+  eq Γ [] τ′ zero = ≅-refl
+  eq (x ∷ Γ) [] τ′ (suc i) = refl ∷ eq Γ [] τ′ i
+  eq Γ (x ∷ Δ) τ′ i = refl ∷ (eq Γ Δ τ′ i)
+
+  fcast-involutive : ∀ {k m n} i → .(k≡m : k ≡ m) → .(m≡n : m ≡ n) → .(k≡n : k ≡ n) → F.cast m≡n (F.cast k≡m i) ≡ F.cast k≡n i
+  fcast-involutive i k≡m m≡n k≡n = toℕ-injective (begin
+    toℕ (F.cast m≡n (F.cast k≡m i)) ≡⟨ toℕ-cast m≡n (F.cast k≡m i) ⟩
+    toℕ (F.cast k≡m i) ≡⟨ toℕ-cast k≡m i ⟩
+    toℕ i ≡˘⟨ toℕ-cast k≡n i ⟩
+    toℕ (F.cast k≡n i) ∎)
+
+wkn₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₁ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₁ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂
+
+wkn₂ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+       Γ , Δ ⊢ e ∶ τ →
+       ∀ τ′ i →
+       Γ , insert Δ i τ′ ⊢ wkn e (inject+ m i) ∶ τ
+wkn₂ Eps τ′ i = Eps
+wkn₂ (Char c) τ′ i = Char c
+wkn₂ Bot τ′ i = Bot
+wkn₂ {m} {n} {Γ} {Δ} (Var {i = j} j≥n) τ′ i =
+  subst (Γ , insert Δ i τ′ ⊢_∶ lookup Γ (reduce≥ j j≥n))
+        (cong Var (toℕ-injective (begin-equality
+          toℕ (suc j) ≡⟨⟩
+          suc (toℕ j) ≡˘⟨ cong toℕ (punchIn-suc i≤j) ⟩
+          toℕ (punchIn (inject+ m i) j) ∎)))
+        (Var (s≤s j≥n))
+  where
+  open ≤-Reasoning
+
+  m<n+1⇒m≤n : ∀ {m n} → m ℕ.< suc n → m ℕ.≤ n
+  m<n+1⇒m≤n (s≤s m≤n) = m≤n
+
+  i≤j : toℕ (inject+ m i) ℕ.≤ toℕ j
+  i≤j = begin
+    toℕ (inject+ m i) ≡˘⟨ toℕ-inject+ m i ⟩
+    toℕ i ≤⟨ m<n+1⇒m≤n (toℕ<n i) ⟩
+    n ≤⟨ j≥n ⟩
+    toℕ j ∎
+
+  punchIn-suc : ∀ {m i j} → toℕ i ℕ.≤ toℕ j → punchIn {m} i j ≡ suc j
+  punchIn-suc {_} {zero} {j} i≤j = refl
+  punchIn-suc {_} {suc i} {suc j} (s≤s i≤j) = cong suc (punchIn-suc i≤j)
+wkn₂ (Fix Γ,τ∷Δ⊢e∶τ) τ′ i = Fix (wkn₂ Γ,τ∷Δ⊢e∶τ τ′ (suc i))
+wkn₂ {m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) τ′ i =
+  Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ τ′ i)
+      (subst (insert Δ i τ′ ++ Γ , [] ⊢_∶ τ₂)
+             (begin
+               cast refl (cast refl (wkn e₂ (F.cast refl (inject+ m i)))) ≡⟨ cast-inverse (wkn e₂ (F.cast refl (inject+ m i))) refl refl ⟩
+               wkn e₂ (F.cast refl (inject+ m i)) ≡⟨ cong (wkn e₂) (toℕ-injective (toℕ-cast refl (inject+ m i))) ⟩
+               wkn e₂ (inject+ m i) ∎)
+             (cast₁ (≅-reflexive (eq Γ Δ τ′ i)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ τ′ (inject+ m i))))
+      τ₁⊛τ₂
+  where
+  open ≡-Reasoning
+
+  eq : ∀ {a A m n} Γ Δ τ i → insert (Δ ++ Γ) (inject+ m i) τ ≡ insert {a} {A} {n} Δ i τ ++ Γ
+  eq Γ Δ τ zero = refl
+  eq Γ (_ ∷ Δ) τ (suc i) = cong₂ _∷_ refl (eq Γ Δ τ i)
+wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₂ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂