------------------------------------------------------------------------
-- The logical relation is closed under weakening
------------------------------------------------------------------------

open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.LogicalRelation.Weakening
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  {{eqrel : EqRelSet R}}
  where

open EqRelSet {{...}}
open Type-restrictions R

open import Definition.Untyped M as U hiding (wk; K)
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Inversion M
open import Definition.Untyped.Properties M
open import Definition.Typed.Inversion R
open import Definition.Typed.Properties R
open import Definition.Typed.Weakening R as T hiding (wk; wkEq; wkTerm; wkEqTerm)
open import Definition.Typed.Well-formed R
open import Definition.LogicalRelation R ⦃ eqrel ⦄
open import Definition.LogicalRelation.Irrelevance R ⦃ eqrel ⦄
open import Definition.LogicalRelation.Properties R ⦃ eqrel ⦄
open import Definition.LogicalRelation.Weakening.Restricted R ⦃ eqrel ⦄

open import Tools.Empty
open import Tools.Function
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality

private
  variable
    m n : Nat
    ρ : Wk m n
    Γ Δ : Con Term m
    A B t t′ u u′ : Term m
    l : Universe-level
    s : Strength

-- Weakening of neutrals in WHNF

wkEqTermNe : ∀ {k k′ A} → ρ ∷ʷ Δ ⊇ Γ
           → Γ ⊩neNf k ≡ k′ ∷ A → Δ ⊩neNf U.wk ρ k ≡ U.wk ρ k′ ∷ U.wk ρ A
wkEqTermNe {ρ} [ρ] (neNfₜ₌ inc neK neM k≡m) =
  neNfₜ₌ inc (wkNeutral ρ neK) (wkNeutral ρ neM) (~-wk [ρ] k≡m)

-- Weakening of reducible levels

mutual
  wkTermLevel : ρ ∷ʷ Δ ⊇ Γ
              → Γ ⊩Level t ∷Level
              → Δ ⊩Level U.wk ρ t ∷Level
  wkTermLevel [ρ] (term d prop) =
    term (wkRed*Term [ρ] d) (wkLevel-prop [ρ] prop)
  wkTermLevel [ρ] (literal not-ok _ t-lit) =
    literal not-ok (wf-∷ʷ⊇ [ρ]) (wk-Level-literal .proj₁ t-lit)

  wkLevel-prop : ρ ∷ʷ Δ ⊇ Γ
               → Level-prop Γ t
               → Level-prop Δ (U.wk ρ t)
  wkLevel-prop [ρ] (zeroᵘᵣ ok)   = zeroᵘᵣ ok
  wkLevel-prop [ρ] (sucᵘᵣ ok ⊩t) = sucᵘᵣ ok (wkTermLevel [ρ] ⊩t)
  wkLevel-prop [ρ] (neLvl ⊩t)    = neLvl (wkneLevel-prop [ρ] ⊩t)

  wkneLevel-prop : ρ ∷ʷ Δ ⊇ Γ
                 → neLevel-prop Γ t
                 → neLevel-prop Δ (U.wk ρ t)
  wkneLevel-prop [ρ] (supᵘˡᵣ x y) = supᵘˡᵣ (wkneLevel-prop [ρ] x) (wkTermLevel [ρ] y)
  wkneLevel-prop [ρ] (supᵘʳᵣ x y) = supᵘʳᵣ (wkTermLevel [ρ] x) (wkneLevel-prop [ρ] y)
  wkneLevel-prop [ρ] (ne x) = ne (wkEqTermNe [ρ] x)

mutual
  wkEqTermLevel : ρ ∷ʷ Δ ⊇ Γ
                → Γ ⊩Level t ≡ u ∷Level
                → Δ ⊩Level U.wk ρ t ≡ U.wk ρ u ∷Level
  wkEqTermLevel [ρ] (term d d′ prop) =
    term (wkRed*Term [ρ] d) (wkRed*Term [ρ] d′)
      (wk[Level]-prop [ρ] prop)
  wkEqTermLevel [ρ] (literal! not-ok _ t-lit) =
    literal! not-ok (wf-∷ʷ⊇ [ρ]) (wk-Level-literal .proj₁ t-lit)

  wk[Level]-prop : ρ ∷ʷ Δ ⊇ Γ
                 → [Level]-prop Γ t u
                 → [Level]-prop Δ (U.wk ρ t) (U.wk ρ u)
  wk[Level]-prop ρ (sucᵘᵣ ok [t≡u]) = sucᵘᵣ ok (wkEqTermLevel ρ [t≡u])
  wk[Level]-prop ρ (zeroᵘᵣ ok) = zeroᵘᵣ ok
  wk[Level]-prop ρ (neLvl x) = neLvl (wk[neLevel]-prop ρ x)
  wk[Level]-prop ρ (supᵘ-subᵣ x y) = supᵘ-subᵣ (wkneLevel-prop ρ x) (wkEqTermLevel ρ y)
  wk[Level]-prop [ρ] (sym u≡t) = sym (wk[Level]-prop [ρ] u≡t)
  wk[Level]-prop [ρ] (trans t≡u u≡v) = trans (wk[Level]-prop [ρ] t≡u) (wk[Level]-prop [ρ] u≡v)

  wk[neLevel]-prop : ρ ∷ʷ Δ ⊇ Γ
                   → [neLevel]-prop Γ t u
                   → [neLevel]-prop Δ (U.wk ρ t) (U.wk ρ u)
  wk[neLevel]-prop [ρ] (supᵘˡᵣ t≡u x) = supᵘˡᵣ (wk[neLevel]-prop [ρ] t≡u) (wkEqTermLevel [ρ] x)
  wk[neLevel]-prop [ρ] (supᵘʳᵣ x t≡u) = supᵘʳᵣ (wkEqTermLevel [ρ] x) (wk[neLevel]-prop [ρ] t≡u)
  wk[neLevel]-prop [ρ] (supᵘ-zeroʳᵣ [u]) = supᵘ-zeroʳᵣ (wkneLevel-prop [ρ] [u])
  wk[neLevel]-prop [ρ] (supᵘ-assoc¹ᵣ x y z) = supᵘ-assoc¹ᵣ (wkneLevel-prop [ρ] x) (wkTermLevel [ρ] y) (wkTermLevel [ρ] z)
  wk[neLevel]-prop [ρ] (supᵘ-assoc²ᵣ x y z) = supᵘ-assoc²ᵣ (wkTermLevel [ρ] x) (wkneLevel-prop [ρ] y) (wkTermLevel [ρ] z)
  wk[neLevel]-prop [ρ] (supᵘ-assoc³ᵣ x y z) = supᵘ-assoc³ᵣ (wkTermLevel [ρ] x) (wkTermLevel [ρ] y) (wkneLevel-prop [ρ] z)
  wk[neLevel]-prop [ρ] (supᵘ-comm¹ᵣ x x₁ x₂ x₃) = supᵘ-comm¹ᵣ (wkneLevel-prop [ρ] x) (wkEqTermLevel [ρ] x₁) (wkneLevel-prop [ρ] x₂) (wkEqTermLevel [ρ] x₃)
  wk[neLevel]-prop [ρ] (supᵘ-comm²ᵣ x x₁ x₂) = supᵘ-comm²ᵣ (wkTermLevel [ρ] x) (wkEqTermLevel [ρ] x₁) (wkneLevel-prop [ρ] x₂)
  wk[neLevel]-prop [ρ] (supᵘ-idemᵣ x y) = supᵘ-idemᵣ (wkneLevel-prop [ρ] x) (wkEqTermLevel [ρ] y)
  wk[neLevel]-prop [ρ] (ne x) = ne (wkEqTermNe [ρ] x)

opaque
  unfolding ↑ⁿ_

  -- Weakening preserves level realisation.

  mutual
    wk-↑ⁿ
      : ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
      → (t≡u : Γ ⊩Level t ∷Level)
      → (wk-t≡u′ : Δ ⊩Level t′ ∷Level)
      → t′ PE.≡ U.wk ρ t
      → ↑ⁿ wk-t≡u′ PE.≡ ↑ⁿ t≡u
    wk-↑ⁿ {ρ} [ρ] (term d prop) (term d′ prop′) PE.refl =
      case whrDet*Term (d′ , level prop′) (wkRed*Term [ρ] d , wkWhnf ρ (level prop)) of λ {
        PE.refl →
      wk-↑ⁿ-prop [ρ] prop prop′ PE.refl }
    wk-↑ⁿ _ (literal _ _ t-lit) (literal _ _ t′-lit) PE.refl =
      size-of-Level t′-lit                           ≡⟨ PE.cong size-of-Level Level-literal-propositional ⟩
      size-of-Level (wk-Level-literal .proj₁ t-lit)  ≡⟨ size-of-Level-wk-Level-literal ⟩
      size-of-Level t-lit                            ∎
    wk-↑ⁿ _ (literal not-ok _ _) (term ⇒∷Level _) _ =
      ⊥-elim $ not-ok $
      inversion-Level-⊢ (wf-⊢≡∷ (subset*Term ⇒∷Level) .proj₁)
    wk-↑ⁿ _ (term ⇒∷Level _) (literal not-ok _ _) _ =
      ⊥-elim $ not-ok $
      inversion-Level-⊢ (wf-⊢≡∷ (subset*Term ⇒∷Level) .proj₁)

    wk-↑ⁿ-prop
      : ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
      → (t≡u : Level-prop Γ t)
      → (wk-t≡u : Level-prop Δ t′)
      → t′ PE.≡ U.wk ρ t
      → ↑ⁿ-prop wk-t≡u PE.≡ ↑ⁿ-prop t≡u
    wk-↑ⁿ-prop [ρ] (zeroᵘᵣ _) ⊩t′ PE.refl = ↑ⁿ-prop-zeroᵘ ⊩t′
    wk-↑ⁿ-prop [ρ] (sucᵘᵣ _ ⊩t) ⊩t′ PE.refl =
      let ⊩wk-t , ↑t′≡ = ↑ⁿ-prop-sucᵘ ⊩t′
      in PE.trans ↑t′≡ (PE.cong 1+ (wk-↑ⁿ [ρ] ⊩t ⊩wk-t PE.refl))
    wk-↑ⁿ-prop [ρ] (neLvl ⊩t) (zeroᵘᵣ _) p =
      case wk-zeroᵘ (PE.sym p) of λ {
        PE.refl →
      case nelevel ⊩t of λ {
        (ne ()) }}
    wk-↑ⁿ-prop [ρ] (neLvl ⊩t) (sucᵘᵣ _ _) p =
      case wk-sucᵘ (PE.sym p) of λ {
        (_ , PE.refl , PE.refl) →
      case nelevel ⊩t of λ {
        (ne ()) }}
    wk-↑ⁿ-prop [ρ] (neLvl x) (neLvl y) PE.refl = wk-↑ⁿ-neprop [ρ] x y PE.refl

    wk-↑ⁿ-neprop
      : ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
      → (t≡u : neLevel-prop Γ t)
      → (wk-t≡u : neLevel-prop Δ t′)
      → t′ PE.≡ U.wk ρ t
      → ↑ⁿ-neprop wk-t≡u PE.≡ ↑ⁿ-neprop t≡u
    wk-↑ⁿ-neprop [ρ] (supᵘˡᵣ t≡u x) (supᵘˡᵣ wk-t≡u x₁) PE.refl =
      PE.cong₂ _⊔_ (wk-↑ⁿ-neprop [ρ] t≡u wk-t≡u PE.refl) (wk-↑ⁿ [ρ] x x₁ PE.refl)
    wk-↑ⁿ-neprop [ρ] (supᵘʳᵣ x t≡u) (supᵘʳᵣ x₁ wk-t≡u) PE.refl =
      PE.cong₂ _⊔_ (PE.cong 1+ (wk-↑ⁿ [ρ] x x₁ PE.refl)) (wk-↑ⁿ-neprop [ρ] t≡u wk-t≡u PE.refl)
    wk-↑ⁿ-neprop [ρ] (ne _) (ne _) PE.refl = PE.refl
    wk-↑ⁿ-neprop [ρ] (supᵘˡᵣ t≡u x) (supᵘʳᵣ x₁ wk-t≡u) p =
      case supᵘ-PE-injectivity p of λ { (q , PE.refl) →
      case wk-sucᵘ (PE.sym q) of λ { (_ , PE.refl , PE.refl) →
      case nelevel t≡u of λ { (ne ()) } } }
    wk-↑ⁿ-neprop [ρ] (supᵘˡᵣ t≡u x) (ne (neNfₜ₌ _ () neM k≡m)) PE.refl
    wk-↑ⁿ-neprop [ρ] (supᵘʳᵣ x t≡u) (supᵘˡᵣ wk-t≡u x₁) PE.refl =
      case nelevel wk-t≡u of λ { (ne ()) }
    wk-↑ⁿ-neprop [ρ] (supᵘʳᵣ x t≡u) (ne (neNfₜ₌ _ () neM k≡m)) PE.refl
    wk-↑ⁿ-neprop [ρ] (ne (neNfₜ₌ _ neK _ _)) (supᵘˡᵣ wk-t≡u x₁) p =
      case wk-supᵘ (PE.sym p) of λ { (_ , _ , PE.refl , _ , _) →
      case neK of λ () }
    wk-↑ⁿ-neprop [ρ] (ne (neNfₜ₌ _ neK _ _)) (supᵘʳᵣ x₁ wk-t≡u) p =
      case wk-supᵘ (PE.sym p) of λ { (_ , _ , PE.refl , _ , _) →
      case neK of λ () }

  wk-↑ᵘ
    : ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
    → {t≡u : Γ ⊩Level t ∷Level}
    → {wk-t≡u′ : Δ ⊩Level t′ ∷Level}
    → t′ PE.≡ U.wk ρ t
    → ↑ᵘ wk-t≡u′ PE.≡ ↑ᵘ t≡u
  wk-↑ᵘ [ρ] {t≡u} {wk-t≡u′} eq = PE.cong 0ᵘ+_ (wk-↑ⁿ [ρ] t≡u wk-t≡u′ eq)

-- Weakening of reducible natural numbers

mutual
  wkEqTermℕ : ∀ {t u} → ρ ∷ʷ Δ ⊇ Γ
            → Γ ⊩ℕ t ≡ u ∷ℕ
            → Δ ⊩ℕ U.wk ρ t ≡ U.wk ρ u ∷ℕ
  wkEqTermℕ {ρ = ρ} [ρ] (ℕₜ₌ k k′ d d′ t≡u prop) =
    ℕₜ₌ (U.wk ρ k) (U.wk ρ k′) (wkRed*Term [ρ] d)
        (wkRed*Term [ρ] d′) (≅ₜ-wk [ρ] t≡u)
        (wk[Natural]-prop [ρ] prop)

  wk[Natural]-prop : ∀ {n n′} → ρ ∷ʷ Δ ⊇ Γ
                   → [Natural]-prop Γ n n′
                   → [Natural]-prop Δ (U.wk ρ n) (U.wk ρ n′)
  wk[Natural]-prop ρ (sucᵣ [n≡n′]) = sucᵣ (wkEqTermℕ ρ [n≡n′])
  wk[Natural]-prop ρ zeroᵣ = zeroᵣ
  wk[Natural]-prop ρ (ne x) = ne (wkEqTermNe ρ x)

-- Empty

wk[Empty]-prop : ∀ {n n′} → ρ ∷ʷ Δ ⊇ Γ
  → [Empty]-prop Γ n n′
  → [Empty]-prop Δ (U.wk ρ n) (U.wk ρ n′)
wk[Empty]-prop ρ (ne x) = ne (wkEqTermNe ρ x)

wkEqTermEmpty : ∀ {t u} → ρ ∷ʷ Δ ⊇ Γ
  → Γ ⊩Empty t ≡ u ∷Empty
  → Δ ⊩Empty U.wk ρ t ≡ U.wk ρ u ∷Empty
wkEqTermEmpty {ρ} [ρ] (Emptyₜ₌ k k′ d d′ t≡u prop) =
  Emptyₜ₌ (U.wk ρ k) (U.wk ρ k′) (wkRed*Term [ρ] d)
      (wkRed*Term [ρ] d′) (≅ₜ-wk [ρ] t≡u) (wk[Empty]-prop [ρ] prop)

-- Unit
wkUnit : ∀ {s} ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
       → Γ ⊩Unit⟨ s ⟩ A
       → Δ ⊩Unit⟨ s ⟩ U.wk ρ A
wkUnit {ρ} [ρ] (Unitᵣ D ok) = Unitᵣ (wkRed* [ρ] D) ok

wkEqUnit : ∀ {s} ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
         → Γ ⊩Unit⟨ s ⟩ A ≡ B
         → Δ ⊩Unit⟨ s ⟩ U.wk ρ A ≡ U.wk ρ B
wkEqUnit [ρ] (Unit₌ D) = Unit₌ (wkRed* [ρ] D)

wk[Unit]-prop′ : ∀ {t u} ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
               → [Unit]-prop′ Γ 𝕨 t u
               → [Unit]-prop′ Δ 𝕨 (U.wk ρ t) (U.wk ρ u)
wk[Unit]-prop′ [ρ] starᵣ = starᵣ
wk[Unit]-prop′ [ρ] (ne x) = ne (wkEqTermNe [ρ] x)

-- Weakening for [Unit]-prop.
wk[Unit]-prop :
  ρ ∷ʷ Δ ⊇ Γ →
  [Unit]-prop Γ s t u →
  [Unit]-prop Δ s (U.wk ρ t) (U.wk ρ u)
wk[Unit]-prop ρ (Unitₜ₌ʷ prop no-η) =
  Unitₜ₌ʷ (wk[Unit]-prop′ ρ prop) no-η
wk[Unit]-prop ρ (Unitₜ₌ˢ η) =
  Unitₜ₌ˢ η

wkEqTermUnit : ∀ {t u s} ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
             → Γ ⊩Unit⟨ s ⟩ t ≡ u ∷Unit
             → Δ ⊩Unit⟨ s ⟩ U.wk ρ t ≡ U.wk ρ u ∷Unit
wkEqTermUnit {ρ} [ρ] (Unitₜ₌ u₁ u₂ ↘u₁ ↘u₂ prop) =
  Unitₜ₌ (U.wk ρ u₁) (U.wk ρ u₂) (wkRed↘Term [ρ] ↘u₁) (wkRed↘Term [ρ] ↘u₂)
    (wk[Unit]-prop [ρ] prop)

-- U
wkU : ∀ ([ρ] : ρ ∷ʷ Δ ⊇ Γ)
    → Γ ⊩′⟨ l ⟩U A
    → Δ ⊩′⟨ l ⟩U U.wk ρ A
wkU {ρ} {l} [ρ] (Uᵣ l′ [l′] l′< D) = Uᵣ (U.wk ρ l′)
  (wkTermLevel [ρ] [l′])
  (PE.subst (_<ᵘ l) (PE.sym (wk-↑ᵘ [ρ] PE.refl)) l′<)
  (wkRed* [ρ] D)

-- Weakening of the logical relation

record WkKit (l : Universe-level) : Set a where
  field
    wk :
      {ρ : Wk m n} →
      ρ ∷ʷʳ Δ ⊇ Γ → Γ ⊩⟨ l ⟩ A → Δ ⊩⟨ l ⟩ U.wk ρ A

    wkEq :
      ([ρ] : ρ ∷ʷʳ Δ ⊇ Γ) ([A] : Γ ⊩⟨ l ⟩ A) →
      Γ ⊩⟨ l ⟩ A ≡ B / [A] →
      Δ ⊩⟨ l ⟩ U.wk ρ A ≡ U.wk ρ B / wk [ρ] [A]

    wkEqTerm :
      ([ρ] : ρ ∷ʷʳ Δ ⊇ Γ) ([A] : Γ ⊩⟨ l ⟩ A) →
      Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A] →
      Δ ⊩⟨ l ⟩ U.wk ρ t ≡ U.wk ρ u ∷ U.wk ρ A / wk [ρ] [A]

  wkTerm :
    ([ρ] : ρ ∷ʷʳ Δ ⊇ Γ) ([A] : Γ ⊩⟨ l ⟩ A) →
    Γ ⊩⟨ l ⟩ t ∷ A / [A] →
    Δ ⊩⟨ l ⟩ U.wk ρ t ∷ U.wk ρ A / wk [ρ] [A]
  wkTerm ⊩A ⊩t = wkEqTerm ⊩A ⊩t

private module Weakening (l : Universe-level) (rec : ∀ {l′} → l′ <ᵘ l → WkKit l′) where

  module Rec {l′} (l′< : l′ <ᵘ l) = WkKit (rec l′<)

  wk :
    {ρ : Wk m n} →
    ρ ∷ʷʳ Δ ⊇ Γ → Γ ⊩⟨ l ⟩ A → Δ ⊩⟨ l ⟩ U.wk ρ A

  wkEq :
    ([ρ] : ρ ∷ʷʳ Δ ⊇ Γ) ([A] : Γ ⊩⟨ l ⟩ A) →
    Γ ⊩⟨ l ⟩ A ≡ B / [A] →
    Δ ⊩⟨ l ⟩ U.wk ρ A ≡ U.wk ρ B / wk [ρ] [A]

  wkEqTerm :
    ([ρ] : ρ ∷ʷʳ Δ ⊇ Γ) ([A] : Γ ⊩⟨ l ⟩ A) →
    Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A] →
    Δ ⊩⟨ l ⟩ U.wk ρ t ≡ U.wk ρ u ∷ U.wk ρ A / wk [ρ] [A]

  wkTerm :
    ([ρ] : ρ ∷ʷʳ Δ ⊇ Γ) ([A] : Γ ⊩⟨ l ⟩ A) →
    Γ ⊩⟨ l ⟩ t ∷ A / [A] →
    Δ ⊩⟨ l ⟩ U.wk ρ t ∷ U.wk ρ A / wk [ρ] [A]
  wkTerm ⊩A ⊩t = wkEqTerm ⊩A ⊩t

  wk ρ (Levelᵣ D) = Levelᵣ (wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ) D)
  wk ρ (Liftᵣ′ D [k] [F]) =
    let [ρ] = ∷ʷʳ⊇→∷ʷ⊇ ρ
    in Liftᵣ′ (wkRed* [ρ] D) (wkTermLevel [ρ] [k]) (wk ρ [F])
  wk ρ (Uᵣ [A]) = Uᵣ (wkU (∷ʷʳ⊇→∷ʷ⊇ ρ) [A])
  wk ρ (ℕᵣ D) = ℕᵣ (wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ) D)
  wk ρ (Emptyᵣ D) = Emptyᵣ (wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ) D)
  wk ρ (Unitᵣ [A]) = Unitᵣ (wkUnit (∷ʷʳ⊇→∷ʷ⊇ ρ) [A])
  wk {ρ} [ρ] (ne′ inc _ D neK K≡K) =
    let [ρ] = ∷ʷʳ⊇→∷ʷ⊇ [ρ] in
    ne′ inc (U.wk ρ _) (wkRed* [ρ] D) (wkNeutral ρ neK) (≅-wk [ρ] K≡K)
  wk {m} {Δ} {Γ} {A} {ρ} [ρ] (Πᵣ′ F G D A≡A [F] [G] G-ext ok) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
        [F]′ : ∀ {k} {ρ : Wk k m} {ρ′ E}
              ([ρ] : ρ ∷ʷʳ E ⊇ Δ) ([ρ′] : ρ′ ∷ʷʳ Δ ⊇ Γ)
            → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F)
        [F]′ {_} {ρ} {ρ′} [ρ] [ρ′] =
          irrelevance′ (PE.sym (wk-comp ρ ρ′ F)) ([F] ([ρ] •ₜʷʳ [ρ′]))
        [a]′ : ∀ {k} {ρ : Wk k m} {ρ′ E a}
              ([ρ] : ρ ∷ʷʳ E ⊇ Δ) ([ρ′] : ρ′ ∷ʷʳ Δ ⊇ Γ)
              ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′])
            → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F / [F] ([ρ] •ₜʷʳ [ρ′])
        [a]′ {_} {ρ} {ρ′} [ρ] [ρ′] [a] =
          irrelevanceTerm′ (wk-comp ρ ρ′ F) ([F]′ [ρ] [ρ′]) ([F] _) [a]
        [G]′ : ∀ {k} {ρ : Wk k m} {ρ′} {E} {a}
              ([ρ] : ρ ∷ʷʳ E ⊇ Δ) ([ρ′] : ρ′ ∷ʷʳ Δ ⊇ Γ)
              ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′])
            → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ]₀
        [G]′ {_} η η′ [a] = [G] _ ([a]′ η η′ [a])
    in  Πᵣ′ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed* [ρ]′ D)
            (≅-wk [ρ]′ A≡A)
            (λ {_} {ρ₁} [ρ₁] → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                  ([F] _))
            (λ {_} {ρ₁} [ρ₁] [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                      ([G]′ [ρ₁] [ρ] [a]))
            (λ {_} {ρ₁} [ρ₁] [a] [b] [a≡b] →
                let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F)
                              ([F]′ [ρ₁] [ρ]) ([F] _) [a≡b]
                in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                    (wk-comp-subst ρ₁ ρ G)
                                    ([G]′ [ρ₁] [ρ] [a])
                                    (irrelevance′
                                              (wk-comp-subst ρ₁ ρ G)
                                              ([G]′ [ρ₁] [ρ] [a]))
                                    (G-ext _
                                          ([a]′ [ρ₁] [ρ] [a])
                                          ([a]′ [ρ₁] [ρ] [b])
                                          [a≡b]′))
            ok
  wk {m} {Δ} {Γ} {A} {ρ} [ρ] (Σᵣ′ F G D A≡A [F] [G] G-ext ok) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
        [F]′ : ∀ {k} {ρ : Wk k m} {ρ′ E}
              ([ρ] : ρ ∷ʷʳ E ⊇ Δ) ([ρ′] : ρ′ ∷ʷʳ Δ ⊇ Γ)
            → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F)
        [F]′ {_} {ρ} {ρ′} [ρ] [ρ′] =
          irrelevance′ (PE.sym (wk-comp ρ ρ′ F)) ([F] ([ρ] •ₜʷʳ [ρ′]))
        [a]′ : ∀ {k} {ρ : Wk k m} {ρ′ E a}
              ([ρ] : ρ ∷ʷʳ E ⊇ Δ) ([ρ′] : ρ′ ∷ʷʳ Δ ⊇ Γ)
              ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′])
            → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F / [F] ([ρ] •ₜʷʳ [ρ′])
        [a]′ {_} {ρ} {ρ′} [ρ] [ρ′] [a] =
          irrelevanceTerm′ (wk-comp ρ ρ′ F) ([F]′ [ρ] [ρ′]) ([F] _) [a]
        [G]′ : ∀ {k} {ρ : Wk k m} {ρ′ E a}
              ([ρ] : ρ ∷ʷʳ E ⊇ Δ) ([ρ′] : ρ′ ∷ʷʳ Δ ⊇ Γ)
              ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′])
            → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ]₀
        [G]′ {_} η η′ [a] = [G] _ ([a]′ η η′ [a])
    in  Σᵣ′ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed* [ρ]′ D)
            (≅-wk [ρ]′ A≡A)
            (λ {_} {ρ₁} [ρ₁] → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                  ([F] _))
            (λ {_} {ρ₁} [ρ₁] [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                      ([G]′ [ρ₁] [ρ] [a]))
            (λ {_} {ρ₁} [ρ₁] [a] [b] [a≡b] →
                let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F)
                              ([F]′ [ρ₁] [ρ]) ([F] _) [a≡b]
                in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                    (wk-comp-subst ρ₁ ρ G)
                                    ([G]′ [ρ₁] [ρ] [a])
                                    (irrelevance′
                                              (wk-comp-subst ρ₁ ρ G)
                                              ([G]′ [ρ₁] [ρ] [a]))
                                    (G-ext _
                                          ([a]′ [ρ₁] [ρ] [a])
                                          ([a]′ [ρ₁] [ρ] [b])
                                          [a≡b]′))
            ok
  wk ρ∷⊇ (Idᵣ ⊩A) = Idᵣ (record
    { ⇒*Id  = wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ∷⊇) ⇒*Id
    ; ⊩Ty   = wk ρ∷⊇ ⊩Ty
    ; ⊩lhs  = wkTerm ρ∷⊇ ⊩Ty ⊩lhs
    ; ⊩rhs  = wkTerm ρ∷⊇ ⊩Ty ⊩rhs
    })
    where
    open _⊩ₗId_ ⊩A

  wkEq ρ (Levelᵣ D) A≡B = wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ) A≡B
  wkEq ρ (Liftᵣ′ D [k] [F]) (Lift₌ D′ k≡k′ F≡F′) =
    let [ρ] = ∷ʷʳ⊇→∷ʷ⊇ ρ in
    Lift₌ (wkRed* [ρ] D′) (wkEqTermLevel [ρ] k≡k′) (wkEq ρ [F] F≡F′)
  wkEq ρ (Uᵣ′ l [l] l< D) (U₌ k D′ l≡k) =
    let ρ = ∷ʷʳ⊇→∷ʷ⊇ ρ in
    U₌ (U.wk _ k) (wkRed* ρ D′) (wkEqTermLevel ρ l≡k)
  wkEq ρ (ℕᵣ D) A≡B = wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ) A≡B
  wkEq ρ (Emptyᵣ D) A≡B = wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ) A≡B
  wkEq ρ (Unitᵣ′ _ _) A≡B = wkEqUnit (∷ʷʳ⊇→∷ʷ⊇ ρ) A≡B
  wkEq {ρ = ρ} [ρ] (ne′ _ _ _ _ _) (ne₌ inc M D′ neM K≡M) =
    let [ρ] = ∷ʷʳ⊇→∷ʷ⊇ [ρ] in
    ne₌ inc (U.wk ρ M) (wkRed* [ρ] D′) (wkNeutral ρ neM)
      (≅-wk [ρ] K≡M)
  wkEq
    {ρ}
    [ρ] (Πᵣ′ F G D A≡A [F] [G] G-ext _) (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ] in
    B₌ (U.wk ρ F′)
      (U.wk (lift ρ) G′) (T.wkRed* [ρ]′ D′) (≅-wk [ρ]′ A≡B)
      (λ {_} {ρ₁} [ρ₁] → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                            (PE.sym (wk-comp ρ₁ ρ F′))
                            ([F] ([ρ₁] •ₜʷʳ [ρ]))
                            (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                              ([F] _))
                            ([F≡F′] _))
      (λ {_} {ρ₁} [ρ₁] [a] →
          let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F)
                      (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) ([F] _))
                      ([F] _) [a]
          in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                              (wk-comp-subst ρ₁ ρ G′)
                              ([G] _ [a]′)
                              (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                            ([G] _ [a]′))
                              ([G≡G′] _ [a]′))
  wkEq
    {ρ}
    [ρ] (Σᵣ′ F G D A≡A [F] [G] G-ext _) (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ] in
    B₌ (U.wk ρ F′) (U.wk (lift ρ) G′) (T.wkRed* [ρ]′ D′) (≅-wk [ρ]′ A≡B)
      (λ {_} {ρ₁} [ρ₁] → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                            (PE.sym (wk-comp ρ₁ ρ F′))
                            ([F] ([ρ₁] •ₜʷʳ [ρ]))
                            (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                          ([F] _))
                            ([F≡F′] _))
      (λ {_} {ρ₁} [ρ₁] [a] →
          let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F)
                      (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) ([F] _))
                      ([F] _) [a]
          in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                              (wk-comp-subst ρ₁ ρ G′)
                              ([G] _ [a]′)
                              (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                            ([G] _ [a]′))
                              ([G≡G′] _ [a]′))
  wkEq ρ∷⊇ (Idᵣ ⊩A) A≡B = Id₌′
    (wkRed* (∷ʷʳ⊇→∷ʷ⊇ ρ∷⊇) ⇒*Id′)
    (wkEq ρ∷⊇ ⊩Ty Ty≡Ty′)
    (wkEqTerm ρ∷⊇ ⊩Ty lhs≡lhs′)
    (wkEqTerm ρ∷⊇ ⊩Ty rhs≡rhs′)
    where
    open _⊩ₗId_ ⊩A
    open _⊩ₗId_≡_/_ A≡B

  wkEqTerm ρ (Levelᵣ D) [t≡u] = wkEqTermLevel (∷ʷʳ⊇→∷ʷ⊇ ρ) [t≡u]
  wkEqTerm
    {ρ} [ρ] (Uᵣ [U]@(Uᵣ k [k] k< D))
    (Uₜ₌ A B d d′ typeA typeB A≡B [t] [u] [t≡u]) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
        p = wkU [ρ]′ [U] ._⊩₁U_.k<
    in
    Uₜ₌ (U.wk ρ A) (U.wk ρ B) (wkRed*Term [ρ]′ d) (wkRed*Term [ρ]′ d′)
        (wkType ρ typeA) (wkType ρ typeB) (≅ₜ-wk [ρ]′ A≡B)
        (⊩<⇔⊩ p .proj₂ $ PE.subst (flip (_⊩⟨_⟩_ _) _) (PE.sym $ wk-↑ᵘ [ρ]′ PE.refl) $
          Rec.wk k< [ρ] (⊩<⇔⊩ k< .proj₁ [t]))
        (⊩<⇔⊩ p .proj₂ $ PE.subst (flip (_⊩⟨_⟩_ _) _) (PE.sym $ wk-↑ᵘ [ρ]′ PE.refl) $
          Rec.wk k< [ρ] (⊩<⇔⊩ k< .proj₁ [u]))
        (⊩<≡⇔⊩≡ p .proj₂ $ irrelevanceEq _ _ $
          Rec.wkEq k< [ρ] _ (⊩<≡⇔⊩≡ k< .proj₁ [t≡u]))
  wkEqTerm ρ (Liftᵣ′ D [k] [F]) (Liftₜ₌ _ _ t↘ u↘ t≡u) =
    let [ρ] = ∷ʷʳ⊇→∷ʷ⊇ ρ in
    Liftₜ₌ _ _ (wkRed↘Term [ρ] t↘) (wkRed↘Term [ρ] u↘) (wkEqTerm ρ [F] t≡u)
  wkEqTerm ρ (ℕᵣ D) [t≡u] = wkEqTermℕ (∷ʷʳ⊇→∷ʷ⊇ ρ) [t≡u]
  wkEqTerm ρ (Emptyᵣ D) [t≡u] = wkEqTermEmpty (∷ʷʳ⊇→∷ʷ⊇ ρ) [t≡u]
  wkEqTerm ρ (Unitᵣ′ _ _) [t≡u] = wkEqTermUnit (∷ʷʳ⊇→∷ʷ⊇ ρ) [t≡u]
  wkEqTerm {ρ} [ρ] (ne′ _ _ D neK K≡K) (neₜ₌ k m d d′ nf) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ] in
    neₜ₌ (U.wk ρ k) (U.wk ρ m) (wkRed*Term [ρ]′ d)
      (wkRed*Term [ρ]′ d′) (wkEqTermNe [ρ]′ nf)
  wkEqTerm {ρ} [ρ] (Πᵣ′ F G _ _ [F] [G] _ _)
    (Πₜ₌ f g d d′ funcF funcG f≡g [f≡g]) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
    in  Πₜ₌ (U.wk ρ f) (U.wk ρ g)
            (wkRed*Term [ρ]′ d) (wkRed*Term [ρ]′ d′)
            (wkFunction ρ funcF) (wkFunction ρ funcG) (≅ₜ-wk [ρ]′ f≡g)
            (λ {_} {ρ₁} [ρ₁] ⊩v ⊩w v≡w →
              let eq   = wk-comp ρ₁ ρ F
                  [F]₁ = [F] _
                  [F]₂ = irrelevance′ (PE.sym eq) [F]₁
                  ⊩v′  = irrelevanceTerm′ eq [F]₂ [F]₁ ⊩v
                  [G]₁ = [G] _ ⊩v′
                  [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
              in  irrelevanceEqTerm″ (PE.cong (λ y → y ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                      (PE.cong (λ y → y ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                      (wk-comp-subst ρ₁ ρ G)
                                      [G]₁ [G]₂
                    ([f≡g] _ ⊩v′ (irrelevanceTerm′ eq [F]₂ [F]₁ ⊩w)
                        (irrelevanceEqTerm′ eq [F]₂ [F]₁ v≡w)))
  wkEqTerm {ρ} [ρ] [A]@(Bᵣ′ BΣʷ F G _ _ [F] [G] _ _)
          (Σₜ₌ p r d d′ (prodₙ {t = p₁}) prodₙ p≅r
              (PE.refl , PE.refl , PE.refl , PE.refl ,
              [p₁] , [r₁] , [fst≡] , [snd≡])) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
        ρidF≡idρF = begin
                      U.wk ρ (U.wk id F)
                    ≡⟨ PE.cong (U.wk ρ) (wk-id F) ⟩
                      U.wk ρ F
                    ≡⟨ PE.sym (wk-id (U.wk ρ F)) ⟩
                      U.wk id (U.wk ρ F)
                    ∎
        [ρF] = irrelevance′ (PE.sym (wk-comp id ρ F)) ([F] [ρ])
        [ρp₁] = wkTerm [ρ] ([F] _) [p₁]
        [ρp₁]′ = irrelevanceTerm′
                    ρidF≡idρF
                    (wk [ρ] ([F] _)) [ρF]
                    [ρp₁]
        [ρr₁] = wkTerm [ρ] ([F] _) [r₁]
        [ρr₁]′ = irrelevanceTerm′
                    ρidF≡idρF
                    (wk [ρ] ([F] _)) [ρF]
                    [ρr₁]
        [ρfst≡] = wkEqTerm [ρ] ([F] _) [fst≡]
        [ρfst≡]′ = irrelevanceEqTerm′
                    ρidF≡idρF
                    (wk [ρ] ([F] _)) [ρF]
                    [ρfst≡]
        [ρsnd≡] = wkEqTerm [ρ] ([G] _ [p₁]) [snd≡]
        [ρG]′ = irrelevance′ (wk-comp-subst id ρ G)
                  ([G] [ρ]
                    (irrelevanceTerm′ (wk-comp id ρ F)
                        [ρF] ([F] [ρ]) [ρp₁]′))
        ρG-eq = λ t → (begin
                      U.wk ρ (U.wk (lift id) G [ t ]₀)
                    ≡⟨ PE.cong (λ x → U.wk ρ (x [ t ]₀)) (wk-lift-id G) ⟩
                      U.wk ρ (G [ t ]₀)
                    ≡⟨ wk-β G ⟩
                      (U.wk (lift ρ) G) [ U.wk ρ t ]₀
                    ≡⟨ PE.cong (λ x → x [ U.wk ρ t ]₀) (PE.sym (wk-lift-id (U.wk (lift ρ) G))) ⟩
                      (U.wk (lift id) (U.wk (lift ρ) G)) [ U.wk ρ t ]₀
                    ∎)
        [ρsnd≡]′ = irrelevanceEqTerm′
                    (ρG-eq p₁)
                    (wk [ρ] ([G] _ [p₁])) [ρG]′
                    [ρsnd≡]
    in  Σₜ₌ (U.wk ρ p) (U.wk ρ r)
            (wkRed*Term [ρ]′ d) (wkRed*Term [ρ]′ d′)
            (wkProduct ρ prodₙ) (wkProduct ρ prodₙ) (≅ₜ-wk [ρ]′ p≅r)
            (PE.refl , PE.refl , PE.refl , PE.refl ,
            irrelevanceTerm [ρF]
                (irrelevance′ (PE.sym (wk-comp id ρ F)) _) [ρp₁]′ ,
            irrelevanceTerm [ρF]
              (irrelevance′ (PE.sym (wk-comp id ρ F)) _) [ρr₁]′ ,
            irrelevanceEqTerm [ρF]
              (irrelevance′ (PE.sym (wk-comp id ρ F)) _) [ρfst≡]′ ,
            irrelevanceEqTerm [ρG]′
              (irrelevance′ (wk-comp-subst id ρ G) _) [ρsnd≡]′)
  wkEqTerm
    {ρ} [ρ] [A]@(Bᵣ′ BΣʷ _ _ _ _ _ _ _ _)
    (Σₜ₌ p r d d′ (ne x) (ne y) p≅r (inc , p~r)) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
    in  Σₜ₌ (U.wk ρ p) (U.wk ρ r)
            (wkRed*Term [ρ]′ d) (wkRed*Term [ρ]′ d′)
            (wkProduct ρ (ne x)) (wkProduct ρ (ne y)) (≅ₜ-wk [ρ]′ p≅r)
            (inc , ~-wk [ρ]′ p~r)
  wkEqTerm
    {ρ} [ρ] [A]@(Bᵣ′ BΣˢ F G _ _ [F] [G] _ _)
    (Σₜ₌ p r d d′ pProd rProd p≅r ([fstp] , [fstr] , [fst≡] , [snd≡])) =
    let [ρ]′ = ∷ʷʳ⊇→∷ʷ⊇ [ρ]
        ρidF≡idρF = begin
                      U.wk ρ (U.wk id F)
                    ≡⟨ PE.cong (U.wk ρ) (wk-id F) ⟩
                      U.wk ρ F
                    ≡⟨ PE.sym (wk-id (U.wk ρ F)) ⟩
                      U.wk id (U.wk ρ F)
                    ∎
        [ρF] = irrelevance′ (PE.sym (wk-comp id ρ F)) ([F] [ρ])
        [ρfstp] = wkTerm [ρ] ([F] _) [fstp]
        [ρfstp]′ = irrelevanceTerm′
                    ρidF≡idρF
                    (wk [ρ] ([F] _)) [ρF]
                    [ρfstp]
        [ρfstr] = wkTerm [ρ] ([F] _) [fstr]
        [ρfstr]′ = irrelevanceTerm′
                    ρidF≡idρF
                    (wk [ρ] ([F] _)) [ρF]
                    [ρfstr]
        [ρfst≡] = wkEqTerm [ρ] ([F] _) [fst≡]
        [ρfst≡]′ = irrelevanceEqTerm′
                    ρidF≡idρF
                    (wk [ρ] ([F] _)) [ρF]
                    [ρfst≡]
        [ρsnd≡] = wkEqTerm [ρ] ([G] _ [fstp]) [snd≡]
        [ρG]′ = irrelevance′ (wk-comp-subst id ρ G)
                  ([G] [ρ]
                    (irrelevanceTerm′ (wk-comp id ρ F)
                        [ρF] ([F] [ρ]) [ρfstp]′))
        [ρsnd≡]′ = irrelevanceEqTerm′
          (begin
            U.wk ρ (U.wk (lift id) G [ fst _ p ]₀)                    ≡⟨ PE.cong (λ x → U.wk ρ (x [ fst _ p ]₀)) (wk-lift-id G) ⟩
            U.wk ρ (G [ fst _ p ]₀)                                   ≡⟨ wk-β G ⟩
            (U.wk (lift ρ) G) [ fst _ (U.wk ρ p) ]₀                   ≡⟨ PE.cong (λ x → x [ fst _ (U.wk ρ p) ]₀)
                                                                          (PE.sym (wk-lift-id (U.wk (lift ρ) G))) ⟩
            (U.wk (lift id) (U.wk (lift ρ) G)) [ fst _ (U.wk ρ p) ]₀  ∎)
          (wk [ρ] ([G] _ [fstp])) [ρG]′
          [ρsnd≡]
    in  Σₜ₌ (U.wk ρ p) (U.wk ρ r)
            (wkRed*Term [ρ]′ d) (wkRed*Term [ρ]′ d′)
            (wkProduct ρ pProd) (wkProduct ρ rProd) (≅ₜ-wk [ρ]′ p≅r)
            (irrelevanceTerm [ρF]
              (irrelevance′ (PE.sym (wk-comp id ρ F)) _) [ρfstp]′ ,
            irrelevanceTerm [ρF]
              (irrelevance′ (PE.sym (wk-comp id ρ F)) _) [ρfstr]′ ,
            irrelevanceEqTerm [ρF]
              (irrelevance′ (PE.sym (wk-comp id ρ F)) _) [ρfst≡]′ ,
            irrelevanceEqTerm [ρG]′
              (irrelevance′ (wk-comp-subst id ρ G) _) [ρsnd≡]′)
  wkEqTerm ρ∷⊇ (Idᵣ ⊩A) t≡u@(_ , _ , t⇒*t′ , u⇒*u′ , _) =
    let ρ∷⊇′ = ∷ʷʳ⊇→∷ʷ⊇ ρ∷⊇ in
      _ , _
    , wkRed*Term ρ∷⊇′ t⇒*t′
    , wkRed*Term ρ∷⊇′ u⇒*u′
    , (case ⊩Id≡∷-view-inhabited ⊩A t≡u of λ where
        (rfl₌ lhs≡rhs) →
            rflₙ , rflₙ
          , wkEqTerm ρ∷⊇ ⊩Ty lhs≡rhs
        (ne inc t′-n u′-n t′~u′) →
            ne (wkNeutral _ t′-n)
          , ne (wkNeutral _ u′-n)
          , inc
          , ~-wk ρ∷⊇′ t′~u′)
    where
    open _⊩ₗId_ ⊩A

  -- Impossible cases
  wkEqTerm _ (Bᵣ BΣʷ record{}) (Σₜ₌ _ _ _ _ prodₙ (ne _) _ ())
  wkEqTerm _ (Bᵣ BΣʷ record{}) (Σₜ₌ _ _ _ _ (ne _) prodₙ _ ())

private opaque
  wkKit : ∀ l → WkKit l
  wkKit l = <ᵘ-rec WkKit (λ l rec → record { Weakening l rec }) l

module _ {l} where open WkKit (wkKit l) public