------------------------------------------------------------------------
-- Weakening lemmas for the definition context
------------------------------------------------------------------------

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

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

open Type-restrictions R

open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Neutral.Atomic M type-variant
open import Definition.Untyped.Properties M
open import Definition.Untyped.Whnf M type-variant

open import Definition.Typed R
open import Definition.Typed.Properties.Definition.Primitive R
open import Definition.Typed.Properties.Well-formed R
open import Definition.Typed.Weakening R

open import Tools.Function
open import Tools.Nat
open import Tools.Product as Σ
import Tools.PropositionalEquality as PE
open import Tools.Sum

private
  variable
    m n n′ k α : Nat
    ∇ ∇′ ∇″ : DCon (Term 0) _
    ξ : DExt _ _ _
    Γ Δ : Con Term _
    𝓙 : Judgement _
    A A′ t t′ : Term _
    l l₁ l₂ : Lvl _
    V : Set a
    φ : Unfolding _
    ω : Opacity _
    ρ : Wk _ _

------------------------------------------------------------------------
-- Well-typed definition context extensions

data DWkStep (∇ : DCon (Term 0) n) (A : Term 0) (t : Term 0) : Opacity n → Set a where
  opa : Opacity-allowed
      → ∇ » ε ⊢ A
      → Trans φ ∇ » ε ⊢ t ∷ A
      → DWkStep ∇ A t (opa φ)
  tra : ∇ » ε ⊢ t ∷ A
      → DWkStep ∇ A t tra

-- » ∇′ ⊇ ∇ means that ∇′ is a well-formed extension of ∇.

infix 4 »_⊇_

data »_⊇_ : DCon (Term 0) m → DCon (Term 0) n → Set a where
  id   : {∇′ : DCon (Term 0) m} {∇ : DCon (Term 0) n}
         (eq : m PE.≡ n) →
         PE.subst (DCon (Term 0)) eq ∇′ PE.≡ ∇ → » ∇′ ⊇ ∇
  step : » ∇′ ⊇ ∇
       → DWkStep ∇′ A t ω
       → » ∇′ ∙⟨ ω ⟩[ t ∷ A ] ⊇ ∇

pattern id⊇ = id PE.refl PE.refl
pattern stepᵒ ξ⊇ ok ⊢A ⊢t = step ξ⊇ (opa ok ⊢A ⊢t)
pattern stepᵗ ξ⊇ ⊢t = step ξ⊇ (tra ⊢t)
pattern stepᵒ₁ ok ⊢A ⊢t = stepᵒ id⊇ ok ⊢A ⊢t
pattern stepᵗ₁ ⊢t = stepᵗ id⊇ ⊢t

------------------------------------------------------------------------
-- Some lemmas related to _ᵈ•_ and »_⊇_

opaque
  unfolding _ᵈ•_

  -- If ∇ ᵈ• ξ is well-formed, then ∇ ᵈ• ξ is a well-formed extension
  -- of ∇.

  ᵈ•⊇ : » ∇ ᵈ• ξ → » ∇ ᵈ• ξ ⊇ ∇
  ᵈ•⊇ {ξ = idᵉ} _ =
    id⊇
  ᵈ•⊇ {ξ = step ξ _ _ _} ∙ᵒ⟨ ok ⟩[ ⊢t ∷ ⊢A ] =
    stepᵒ (ᵈ•⊇ {ξ = ξ} (defn-wf (wf ⊢A))) ok ⊢A ⊢t
  ᵈ•⊇ {ξ = step ξ _ _ _} ∙ᵗ[ ⊢t ] =
    stepᵗ (ᵈ•⊇ {ξ = ξ} (defn-wf (wf ⊢t))) ⊢t

opaque
  unfolding _ᵈ•_

  -- A corollary of ᵈ•⊇.

  »∙→»∙⊇ :
    » ∇ ∙⟨ ω ⟩[ t ∷ A ] →
    » ∇ ∙⟨ ω ⟩[ t ∷ A ] ⊇ ∇
  »∙→»∙⊇ = ᵈ•⊇ {ξ = step₁ _ _ _}

opaque
  unfolding _ᵈ•_

  -- If ∇′ is an extension of ∇, then there is some extension ξ such
  -- that ∇′ is equal to ∇ ᵈ• ξ.

  »⊇→ :
    {∇ : DCon (Term 0) n} {∇′ : DCon (Term 0) n′} →
    » ∇′ ⊇ ∇ → ∃ λ (ξ : DExt (Term 0) n′ n) → ∇′ PE.≡ ∇ ᵈ• ξ
  »⊇→ id⊇ =
    idᵉ , PE.refl
  »⊇→ (step ∇′⊇∇ _) =
    case »⊇→ ∇′⊇∇ of λ {
      (ξ , PE.refl) →
    step ξ _ _ _ , PE.refl }

opaque

  -- If ∇′ is well-formed, then ∇′ is an extension of ∇ if and only if
  -- there is some extension ξ such that ∇′ is equal to ∇ ᵈ• ξ.

  »⊇⇔ :
    {∇ : DCon (Term 0) n} {∇′ : DCon (Term 0) n′} →
    » ∇′ →
    » ∇′ ⊇ ∇ ⇔ ∃ λ (ξ : DExt (Term 0) n′ n) → ∇′ PE.≡ ∇ ᵈ• ξ
  »⊇⇔ »∇′ = »⊇→ , λ { (_ , PE.refl) → ᵈ•⊇ »∇′ }

------------------------------------------------------------------------
-- Some other lemmas related to »_⊇_

opaque

  -- The relation »_⊇_ is transitive.

  »⊇-trans : » ∇″ ⊇ ∇′ → » ∇′ ⊇ ∇ → » ∇″ ⊇ ∇
  »⊇-trans id⊇            ∇′⊇∇ = ∇′⊇∇
  »⊇-trans (step ∇″⊇∇′ s) ∇′⊇∇ = step (»⊇-trans ∇″⊇∇′ ∇′⊇∇) s

opaque

  -- If ∇′ is a well-formed extension of a well-formed definition
  -- context, then ∇′ is a well-formed definition context.

  wf-»⊇ : » ∇′ ⊇ ∇ → » ∇ → » ∇′
  wf-»⊇ id⊇                 »∇ = »∇
  wf-»⊇ (stepᵒ ξ⊇ ok ⊢A ⊢t) »∇ = ∙ᵒ⟨ ok ⟩[ ⊢t ∷ ⊢A ]
  wf-»⊇ (stepᵗ ξ⊇ ⊢t)       »∇ = ∙ᵗ[ ⊢t ]

opaque

  -- An inversion lemma for »_⊇_.

  inv-»∙⊇ :
    {∇′ : DCon (Term 0) n′} {∇ : DCon (Term 0) n} →
    » ∇′ ∙⟨ ω ⟩[ t ∷ A ] ⊇ ∇ →
    (∃ λ (eq : 1+ n′ PE.≡ n) →
       PE.subst (DCon (Term 0)) eq (∇′ ∙⟨ ω ⟩[ t ∷ A ]) PE.≡ ∇) ⊎
    » ∇′ ⊇ ∇ × DWkStep ∇′ A t ω
  inv-»∙⊇ (id eq₁ eq₂)  = inj₁ (eq₁ , eq₂)
  inv-»∙⊇ (step ∇′⊇∇ s) = inj₂ (∇′⊇∇ , s)

opaque

  -- If ∇′ is an extension of ∇, then the length of ∇′ is at least as
  -- large as the length of ∇.

  ⊇→≤ :
    {∇  : DCon (Term 0) n}
    {∇′ : DCon (Term 0) n′} →
    » ∇′ ⊇ ∇ →
    n ≤ n′
  ⊇→≤ id⊇           = ≤-refl
  ⊇→≤ (step ∇′⊇∇ _) = ≤-trans (⊇→≤ ∇′⊇∇) (n≤1+n _)

opaque

  -- If ∇ is well-formed, then ∇ is an extension of the empty
  -- definition context.

  »⊇ε : » ∇ → » ∇ ⊇ ε
  »⊇ε {∇} =
    (» ∇)                 ≡⟨ PE.cong (»_) $ PE.sym εᵈ•as-DExt ⟩→
    (» ε ᵈ• as-DExt ∇)    →⟨ ᵈ•⊇ ⟩
    » ε ᵈ• as-DExt ∇ ⊇ ε  ≡⟨ PE.cong (»_⊇ _) εᵈ•as-DExt ⟩→
    » ∇ ⊇ ε               □

opaque

  -- A glassification lemma for _»_⊇_.

  glassify-»⊇ : » ∇′ ⊇ ∇ → » glassify ∇′ ⊇ glassify ∇
  glassify-»⊇ id⊇ =
    id⊇
  glassify-»⊇ (stepᵗ ξ⊇ ⊢t) =
    stepᵗ (glassify-»⊇ ξ⊇) (glassify-⊢ ⊢t)
  glassify-»⊇ (stepᵒ ξ⊇ _ _ ⊢t) =
    stepᵗ (glassify-»⊇ ξ⊇)
      (PE.subst₃ _⊢_∷_
         (PE.cong (_» _) glassify-factor) PE.refl PE.refl $
       glassify-⊢ ⊢t)

------------------------------------------------------------------------
-- Weakening for properties of definitions

opaque

  -- A definition weakening lemma for the definition context.

  there*-↦∈ : » ∇′ ⊇ ∇ → α ↦∷ A ∈ ∇ → α ↦∷ A ∈ ∇′
  there*-↦∈ id⊇         α↦t = α↦t
  there*-↦∈ (step ξ⊇ s) α↦t = there (there*-↦∈ ξ⊇ α↦t)

opaque

  -- A definition weakening lemma for the definition context.

  there*-↦∷∈ : » ∇′ ⊇ ∇ → α ↦ t ∷ A ∈ ∇ → α ↦ t ∷ A ∈ ∇′
  there*-↦∷∈ id⊇         α↦t = α↦t
  there*-↦∷∈ (step ξ⊇ s) α↦t = there (there*-↦∷∈ ξ⊇ α↦t)

opaque

  -- A definition weakening lemma for the definition context.

  there*-↦⊘∈ : » ∇′ ⊇ ∇ → α ↦⊘∷ A ∈ ∇ → α ↦⊘∷ A ∈ ∇′
  there*-↦⊘∈ id⊇         α↦t = α↦t
  there*-↦⊘∈ (step ξ⊇ s) α↦t = there (there*-↦⊘∈ ξ⊇ α↦t)

------------------------------------------------------------------------
-- Weakening for typing derivations

private opaque mutual

  -- Single-weakening lemmas for the definition context.

  defn-wk′ : » ∇′ ⊇ ∇ → ∇ »⊢ Γ → ∇′ »⊢ Γ
  defn-wk′ ξ⊇ (ε »∇) = ε (wf-»⊇ ξ⊇ »∇)
  defn-wk′ ξ⊇ (∙ ⊢Γ) = ∙ defn-wk″ ξ⊇ ⊢Γ

  defn-wk″ : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ A → ∇′ » Γ ⊢ A
  defn-wk″ ξ⊇ (Levelⱼ ok ⊢Γ) =
    Levelⱼ ok (defn-wk′ ξ⊇ ⊢Γ)
  defn-wk″ ξ⊇ (Liftⱼ ⊢l ⊢A) =
    Liftⱼ (defn-wkLevel ξ⊇ ⊢l) (defn-wk″ ξ⊇ ⊢A)
  defn-wk″ ξ⊇ (ΠΣⱼ ⊢A ok) = ΠΣⱼ (defn-wk″ ξ⊇ ⊢A) ok
  defn-wk″ ξ⊇ (Idⱼ ⊢A ⊢t₁ ⊢t₂) =
    Idⱼ (defn-wk″ ξ⊇ ⊢A)
        (defn-wkTerm ξ⊇ ⊢t₁)
        (defn-wkTerm ξ⊇ ⊢t₂)
  defn-wk″ ξ⊇ (Quot ok ⊢B) = Quot ok (defn-wk″ ξ⊇ ⊢B)
  defn-wk″ ξ⊇ (univ ⊢A) = univ (defn-wkTerm ξ⊇ ⊢A)

  defn-wkTerm : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ t ∷ A → ∇′ » Γ ⊢ t ∷ A
  defn-wkTerm ξ⊇ (Levelⱼ ⊢Γ ok) =
    Levelⱼ (defn-wk′ ξ⊇ ⊢Γ) ok
  defn-wkTerm ξ⊇ (zeroᵘⱼ ok ⊢Γ) =
    zeroᵘⱼ ok (defn-wk′ ξ⊇ ⊢Γ)
  defn-wkTerm ξ⊇ (sucᵘⱼ ⊢l) =
    sucᵘⱼ (defn-wkTerm ξ⊇ ⊢l)
  defn-wkTerm ξ⊇ (supᵘⱼ ⊢l₁ ⊢l₂) =
    supᵘⱼ (defn-wkTerm ξ⊇ ⊢l₁) (defn-wkTerm ξ⊇ ⊢l₂)
  defn-wkTerm ξ⊇ (Uⱼ ⊢l) =
    Uⱼ (defn-wkLevel ξ⊇ ⊢l)
  defn-wkTerm ξ⊇ (Liftⱼ ⊢l₁ ⊢l₂ ⊢A) =
    Liftⱼ (defn-wkLevel ξ⊇ ⊢l₁) (defn-wkLevel ξ⊇ ⊢l₂)
      (defn-wkTerm ξ⊇ ⊢A)
  defn-wkTerm ξ⊇ (liftⱼ ⊢l ⊢A ⊢t) =
    liftⱼ (defn-wkLevel ξ⊇ ⊢l) (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (lowerⱼ ⊢t) =
    lowerⱼ (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (ΠΣⱼ ⊢l ⊢t₁ ⊢t₂ ok) =
    ΠΣⱼ (defn-wkLevel ξ⊇ ⊢l) (defn-wkTerm ξ⊇ ⊢t₁) (defn-wkTerm ξ⊇ ⊢t₂)
      ok
  defn-wkTerm ξ⊇ (ℕⱼ ⊢Γ) = ℕⱼ (defn-wk′ ξ⊇ ⊢Γ)
  defn-wkTerm ξ⊇ (Emptyⱼ ⊢Γ) = Emptyⱼ (defn-wk′ ξ⊇ ⊢Γ)
  defn-wkTerm ξ⊇ (Unitⱼ ⊢Γ ok) = Unitⱼ (defn-wk′ ξ⊇ ⊢Γ) ok
  defn-wkTerm ξ⊇ (conv ⊢t A≡A′) =
    conv (defn-wkTerm ξ⊇ ⊢t) (defn-wkEq ξ⊇ A≡A′)
  defn-wkTerm ξ⊇ (var ⊢Γ x∈) = var (defn-wk′ ξ⊇ ⊢Γ) x∈
  defn-wkTerm ξ⊇ (defn ⊢Γ α↦t A≡A′) =
    defn (defn-wk′ ξ⊇ ⊢Γ) (there*-↦∈ ξ⊇ α↦t) A≡A′
  defn-wkTerm ξ⊇ (lamⱼ ⊢A ⊢t ok) =
    lamⱼ (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t) ok
  defn-wkTerm ξ⊇ (⊢t₁ ∘ⱼ ⊢t₂) =
    defn-wkTerm ξ⊇ ⊢t₁ ∘ⱼ defn-wkTerm ξ⊇ ⊢t₂
  defn-wkTerm ξ⊇ (prodⱼ ⊢A ⊢t₁ ⊢t₂ ok) =
    prodⱼ (defn-wk″ ξ⊇ ⊢A)
          (defn-wkTerm ξ⊇ ⊢t₁)
          (defn-wkTerm ξ⊇ ⊢t₂)
          ok
  defn-wkTerm ξ⊇ (fstⱼ ⊢A ⊢t) =
    fstⱼ (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (sndⱼ ⊢A ⊢t) =
    sndⱼ (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (prodrecⱼ ⊢A ⊢t ⊢t′) =
    prodrecⱼ (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢t′)
  defn-wkTerm ξ⊇ (zeroⱼ ⊢Γ) = zeroⱼ (defn-wk′ ξ⊇ ⊢Γ)
  defn-wkTerm ξ⊇ (sucⱼ ⊢t) = sucⱼ (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (natrecⱼ ⊢t₀ ⊢tₛ ⊢t) =
    natrecⱼ (defn-wkTerm ξ⊇ ⊢t₀)
            (defn-wkTerm ξ⊇ ⊢tₛ)
            (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (emptyrecⱼ ⊢A ⊢t) =
    emptyrecⱼ (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (starⱼ ⊢Γ ok) = starⱼ (defn-wk′ ξ⊇ ⊢Γ) ok
  defn-wkTerm ξ⊇ (unitrecⱼ ⊢A ⊢t ⊢t′) =
    unitrecⱼ (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢t′)
  defn-wkTerm ξ⊇ (Idⱼ ⊢A ⊢t₁ ⊢t₂) =
    Idⱼ (defn-wkTerm ξ⊇ ⊢A)
        (defn-wkTerm ξ⊇ ⊢t₁)
        (defn-wkTerm ξ⊇ ⊢t₂)
  defn-wkTerm ξ⊇ (rflⱼ ⊢t) = rflⱼ (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (Jⱼ ⊢t ⊢A ⊢tᵣ ⊢t′ ⊢tₚ) =
    Jⱼ (defn-wkTerm ξ⊇ ⊢t)
       (defn-wk″ ξ⊇ ⊢A)
       (defn-wkTerm ξ⊇ ⊢tᵣ)
       (defn-wkTerm ξ⊇ ⊢t′)
       (defn-wkTerm ξ⊇ ⊢tₚ)
  defn-wkTerm ξ⊇ (Kⱼ ⊢A ⊢tᵣ ⊢tₚ ok) =
    Kⱼ (defn-wk″ ξ⊇ ⊢A)
       (defn-wkTerm ξ⊇ ⊢tᵣ)
       (defn-wkTerm ξ⊇ ⊢tₚ)
       ok
  defn-wkTerm ξ⊇ ([]-congⱼ ⊢l ⊢A ⊢t₁ ⊢t₂ ⊢tₚ ok) =
    []-congⱼ (defn-wkLevel ξ⊇ ⊢l)
             (defn-wk″ ξ⊇ ⊢A)
             (defn-wkTerm ξ⊇ ⊢t₁)
             (defn-wkTerm ξ⊇ ⊢t₂)
             (defn-wkTerm ξ⊇ ⊢tₚ) ok
  defn-wkTerm ξ⊇ (Quot ok ⊢l ⊢A ⊢B) =
    Quot ok (defn-wkLevel ξ⊇ ⊢l) (defn-wkTerm ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢B)
  defn-wkTerm ξ⊇ (class ⊢Q ⊢t) =
    class (defn-wk″ ξ⊇ ⊢Q) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkTerm ξ⊇ (resp ⊢Q ⊢t ⊢u ⊢v) =
    resp (defn-wk″ ξ⊇ ⊢Q) (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢u)
      (defn-wkTerm ξ⊇ ⊢v)
  defn-wkTerm ξ⊇ (set ⊢Q ⊢t ⊢u ⊢v ⊢w) =
    set (defn-wk″ ξ⊇ ⊢Q) (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢u)
      (defn-wkTerm ξ⊇ ⊢v) (defn-wkTerm ξ⊇ ⊢w)
  defn-wkTerm ξ⊇ (qrec ⊢C ⊢t ⊢u ⊢v ⊢w) =
    qrec (defn-wk″ ξ⊇ ⊢C) (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢u)
      (defn-wkTerm ξ⊇ ⊢v) (defn-wkTerm ξ⊇ ⊢w)

  defn-wkLevel : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ l ∷Level → ∇′ » Γ ⊢ l ∷Level
  defn-wkLevel ∇′⊇∇ (term ok ⊢l) =
    term ok (defn-wkTerm ∇′⊇∇ ⊢l)
  defn-wkLevel ∇′⊇∇ (literal ok ⊢Γ) =
    literal ok (defn-wk′ ∇′⊇∇ ⊢Γ)

  defn-wkEq : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ A ≡ A′ → ∇′ » Γ ⊢ A ≡ A′
  defn-wkEq ξ⊇ (univ A≡A′) = univ (defn-wkEqTerm ξ⊇ A≡A′)
  defn-wkEq ξ⊇ (refl ⊢A) = refl (defn-wk″ ξ⊇ ⊢A)
  defn-wkEq ξ⊇ (sym A≡A′) = sym (defn-wkEq ξ⊇ A≡A′)
  defn-wkEq ξ⊇ (trans A≡A′ A′≡A″) =
    trans (defn-wkEq ξ⊇ A≡A′) (defn-wkEq ξ⊇ A′≡A″)
  defn-wkEq ξ⊇ (U-cong l₁≡l₂) =
    U-cong (defn-wkEqTerm ξ⊇ l₁≡l₂)
  defn-wkEq ξ⊇ (Lift-cong l₁≡l₂ A₁≡A₂) =
    Lift-cong (defn-wkEqLevel ξ⊇ l₁≡l₂) (defn-wkEq ξ⊇ A₁≡A₂)
  defn-wkEq ξ⊇ (ΠΣ-cong A₁≡A₂ B₁≡B₂ ok) =
    ΠΣ-cong (defn-wkEq ξ⊇ A₁≡A₂) (defn-wkEq ξ⊇ B₁≡B₂) ok
  defn-wkEq ξ⊇ (Id-cong A≡A′ t₁≡t₂ u₁≡u₂) =
    Id-cong (defn-wkEq ξ⊇ A≡A′)
            (defn-wkEqTerm ξ⊇ t₁≡t₂)
            (defn-wkEqTerm ξ⊇ u₁≡u₂)
  defn-wkEq ξ⊇ (Quot-cong ok A₁≡A₂ B₁≡B₂) =
    Quot-cong ok (defn-wkEq ξ⊇ A₁≡A₂) (defn-wkEq ξ⊇ B₁≡B₂)

  defn-wkEqTerm : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ t ≡ t′ ∷ A → ∇′ » Γ ⊢ t ≡ t′ ∷ A
  defn-wkEqTerm ξ⊇ (refl ⊢t) = refl (defn-wkTerm ξ⊇ ⊢t)
  defn-wkEqTerm ξ⊇ (sym ⊢A t≡t′) =
    sym (defn-wk″ ξ⊇ ⊢A) (defn-wkEqTerm ξ⊇ t≡t′)
  defn-wkEqTerm ξ⊇ (trans t≡t′ t′≡t″) =
    trans (defn-wkEqTerm ξ⊇ t≡t′) (defn-wkEqTerm ξ⊇ t′≡t″)
  defn-wkEqTerm ξ⊇ (conv t≡t′ A≡A′) =
    conv (defn-wkEqTerm ξ⊇ t≡t′) (defn-wkEq ξ⊇ A≡A′)
  defn-wkEqTerm ξ⊇ (δ-red ⊢Γ α↦t A≡A′ t≡t′) =
    δ-red (defn-wk′ ξ⊇ ⊢Γ) (there*-↦∷∈ ξ⊇ α↦t) A≡A′ t≡t′
  defn-wkEqTerm ξ⊇ (sucᵘ-cong l₁≡l₂) =
    sucᵘ-cong (defn-wkEqTerm ξ⊇ l₁≡l₂)
  defn-wkEqTerm ξ⊇ (supᵘ-cong l₁≡l₃ l₂≡l₄) =
    supᵘ-cong (defn-wkEqTerm ξ⊇ l₁≡l₃) (defn-wkEqTerm ξ⊇ l₂≡l₄)
  defn-wkEqTerm ξ⊇ (supᵘ-zeroˡ ⊢l) =
    supᵘ-zeroˡ (defn-wkTerm ξ⊇ ⊢l)
  defn-wkEqTerm ξ⊇ (supᵘ-sucᵘ ⊢l₁ ⊢l₂) =
    supᵘ-sucᵘ (defn-wkTerm ξ⊇ ⊢l₁) (defn-wkTerm ξ⊇ ⊢l₂)
  defn-wkEqTerm ξ⊇ (supᵘ-assoc ⊢l₁ ⊢l₂ ⊢l₃) =
    supᵘ-assoc (defn-wkTerm ξ⊇ ⊢l₁) (defn-wkTerm ξ⊇ ⊢l₂)
      (defn-wkTerm ξ⊇ ⊢l₃)
  defn-wkEqTerm ξ⊇ (supᵘ-comm ⊢l₁ ⊢l₂) =
    supᵘ-comm (defn-wkTerm ξ⊇ ⊢l₁) (defn-wkTerm ξ⊇ ⊢l₂)
  defn-wkEqTerm ξ⊇ (supᵘ-idem ⊢l) =
    supᵘ-idem (defn-wkTerm ξ⊇ ⊢l)
  defn-wkEqTerm ξ⊇ (supᵘ-sub ⊢l) =
    supᵘ-sub (defn-wkTerm ξ⊇ ⊢l)
  defn-wkEqTerm ξ⊇ (U-cong l₁≡l₂) =
    U-cong (defn-wkEqTerm ξ⊇ l₁≡l₂)
  defn-wkEqTerm ξ⊇ (Lift-cong ⊢l₁ ⊢l₂ l₂≡l₃ A₁≡A₂) =
    Lift-cong (defn-wkLevel ξ⊇ ⊢l₁) (defn-wkLevel ξ⊇ ⊢l₂)
      (defn-wkEqLevel ξ⊇ l₂≡l₃) (defn-wkEqTerm ξ⊇ A₁≡A₂)
  defn-wkEqTerm ξ⊇ (lower-cong t₁≡t₂) =
    lower-cong (defn-wkEqTerm ξ⊇ t₁≡t₂)
  defn-wkEqTerm ξ⊇ (Lift-β ⊢A ⊢t) =
    Lift-β (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkEqTerm ξ⊇ (Lift-η ⊢l ⊢A ⊢t₁ ⊢t₂ lower-t₁≡lower-t₂) =
    Lift-η (defn-wkLevel ξ⊇ ⊢l) (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t₁)
      (defn-wkTerm ξ⊇ ⊢t₂) (defn-wkEqTerm ξ⊇ lower-t₁≡lower-t₂)
  defn-wkEqTerm ξ⊇ (ΠΣ-cong ⊢l t₁≡t₂ u₁≡u₂ ok) =
    ΠΣ-cong (defn-wkLevel ξ⊇ ⊢l) (defn-wkEqTerm ξ⊇ t₁≡t₂)
      (defn-wkEqTerm ξ⊇ u₁≡u₂) ok
  defn-wkEqTerm ξ⊇ (app-cong t₁≡t₂ u₁≡u₂) =
    app-cong (defn-wkEqTerm ξ⊇ t₁≡t₂) (defn-wkEqTerm ξ⊇ u₁≡u₂)
  defn-wkEqTerm ξ⊇ (β-red ⊢A ⊢t ⊢x eq ok) =
    β-red (defn-wk″ ξ⊇ ⊢A)
          (defn-wkTerm ξ⊇ ⊢t)
          (defn-wkTerm ξ⊇ ⊢x)
          eq ok
  defn-wkEqTerm ξ⊇ (η-eq ⊢A ⊢t ⊢t′ t≡t′ ok) =
    η-eq (defn-wk″ ξ⊇ ⊢A)
         (defn-wkTerm ξ⊇ ⊢t)
         (defn-wkTerm ξ⊇ ⊢t′)
         (defn-wkEqTerm ξ⊇ t≡t′)
         ok
  defn-wkEqTerm ξ⊇ (fst-cong ⊢A t≡t′) =
    fst-cong (defn-wk″ ξ⊇ ⊢A) (defn-wkEqTerm ξ⊇ t≡t′)
  defn-wkEqTerm ξ⊇ (snd-cong ⊢A t≡t′) =
    snd-cong (defn-wk″ ξ⊇ ⊢A) (defn-wkEqTerm ξ⊇ t≡t′)
  defn-wkEqTerm ξ⊇ (Σ-β₁ ⊢A ⊢t ⊢t′ eq ok) =
    Σ-β₁ (defn-wk″ ξ⊇ ⊢A)
         (defn-wkTerm ξ⊇ ⊢t)
         (defn-wkTerm ξ⊇ ⊢t′)
         eq ok
  defn-wkEqTerm ξ⊇ (Σ-β₂ ⊢A ⊢t ⊢t′ eq ok) =
    Σ-β₂ (defn-wk″ ξ⊇ ⊢A)
         (defn-wkTerm ξ⊇ ⊢t)
         (defn-wkTerm ξ⊇ ⊢t′)
         eq ok
  defn-wkEqTerm ξ⊇ (Σ-η ⊢A ⊢t ⊢t′ fst≡ snd≡ ok) =
    Σ-η (defn-wk″ ξ⊇ ⊢A)
        (defn-wkTerm ξ⊇ ⊢t)
        (defn-wkTerm ξ⊇ ⊢t′)
        (defn-wkEqTerm ξ⊇ fst≡)
        (defn-wkEqTerm ξ⊇ snd≡)
        ok
  defn-wkEqTerm ξ⊇ (prod-cong ⊢A t₁≡t₂ u₁≡u₂ ok) =
    prod-cong (defn-wk″ ξ⊇ ⊢A)
              (defn-wkEqTerm ξ⊇ t₁≡t₂)
              (defn-wkEqTerm ξ⊇ u₁≡u₂)
              ok
  defn-wkEqTerm ξ⊇ (prodrec-cong A≡A′ t₁≡t₂ u₁≡u₂) =
    prodrec-cong (defn-wkEq ξ⊇ A≡A′) (defn-wkEqTerm ξ⊇ t₁≡t₂)
      (defn-wkEqTerm ξ⊇ u₁≡u₂)
  defn-wkEqTerm ξ⊇ (prodrec-β ⊢A ⊢t₁ ⊢t₂ ⊢tᵣ eq) =
    prodrec-β (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t₁) (defn-wkTerm ξ⊇ ⊢t₂)
      (defn-wkTerm ξ⊇ ⊢tᵣ) eq
  defn-wkEqTerm ξ⊇ (suc-cong t≡t′) =
    suc-cong (defn-wkEqTerm ξ⊇ t≡t′)
  defn-wkEqTerm ξ⊇ (natrec-cong A≡A′ 0≡ s≡ t≡t′) =
    natrec-cong (defn-wkEq ξ⊇ A≡A′)
                (defn-wkEqTerm ξ⊇ 0≡)
                (defn-wkEqTerm ξ⊇ s≡)
                (defn-wkEqTerm ξ⊇ t≡t′)
  defn-wkEqTerm ξ⊇ (natrec-zero ⊢t₀ ⊢tₛ) =
    natrec-zero (defn-wkTerm ξ⊇ ⊢t₀) (defn-wkTerm ξ⊇ ⊢tₛ)
  defn-wkEqTerm ξ⊇ (natrec-suc ⊢t₀ ⊢tₛ ⊢t) =
    natrec-suc (defn-wkTerm ξ⊇ ⊢t₀)
               (defn-wkTerm ξ⊇ ⊢tₛ)
               (defn-wkTerm ξ⊇ ⊢t)
  defn-wkEqTerm ξ⊇ (emptyrec-cong A≡A′ t≡t′) =
    emptyrec-cong (defn-wkEq ξ⊇ A≡A′) (defn-wkEqTerm ξ⊇ t≡t′)
  defn-wkEqTerm ξ⊇ (unitrec-cong A≡A′ t≡t′ r≡ no-η) =
    unitrec-cong (defn-wkEq ξ⊇ A≡A′) (defn-wkEqTerm ξ⊇ t≡t′)
      (defn-wkEqTerm ξ⊇ r≡) no-η
  defn-wkEqTerm ξ⊇ (unitrec-β ⊢A ⊢t no-η) =
    unitrec-β (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t) no-η
  defn-wkEqTerm ξ⊇ (unitrec-β-η ⊢A ⊢t ⊢tᵣ η) =
    unitrec-β-η (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t)
      (defn-wkTerm ξ⊇ ⊢tᵣ) η
  defn-wkEqTerm ξ⊇ (η-unit ⊢t ⊢t′ η) =
    η-unit (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢t′) η
  defn-wkEqTerm ξ⊇ (Id-cong A≡A′ t₁≡t₂ u₁≡u₂) =
    Id-cong (defn-wkEqTerm ξ⊇ A≡A′)
            (defn-wkEqTerm ξ⊇ t₁≡t₂)
            (defn-wkEqTerm ξ⊇ u₁≡u₂)
  defn-wkEqTerm ξ⊇ (J-cong A≡A′ ⊢t t≡t′ B₁≡B₂ r≡ x≡ p≡) =
    J-cong (defn-wkEq ξ⊇ A≡A′)
           (defn-wkTerm ξ⊇ ⊢t)
           (defn-wkEqTerm ξ⊇ t≡t′)
           (defn-wkEq ξ⊇ B₁≡B₂)
           (defn-wkEqTerm ξ⊇ r≡)
           (defn-wkEqTerm ξ⊇ x≡)
           (defn-wkEqTerm ξ⊇ p≡)
  defn-wkEqTerm ξ⊇ (K-cong A≡A′ t≡t′ B₁≡B₂ r≡ p≡ ok) =
    K-cong (defn-wkEq ξ⊇ A≡A′)
           (defn-wkEqTerm ξ⊇ t≡t′)
           (defn-wkEq ξ⊇ B₁≡B₂)
           (defn-wkEqTerm ξ⊇ r≡)
           (defn-wkEqTerm ξ⊇ p≡)
           ok
  defn-wkEqTerm ξ⊇ ([]-cong-cong l₁≡l₂ A≡A′ t₁≡t₂ u₁≡u₂ p≡p′ ok) =
    []-cong-cong (defn-wkEqLevel ξ⊇ l₁≡l₂)
                 (defn-wkEq ξ⊇ A≡A′)
                 (defn-wkEqTerm ξ⊇ t₁≡t₂)
                 (defn-wkEqTerm ξ⊇ u₁≡u₂)
                 (defn-wkEqTerm ξ⊇ p≡p′) ok
  defn-wkEqTerm ξ⊇ (J-β ⊢t ⊢A ⊢tᵣ eq) =
    J-β (defn-wkTerm ξ⊇ ⊢t)
        (defn-wk″ ξ⊇ ⊢A)
        (defn-wkTerm ξ⊇ ⊢tᵣ)
        eq
  defn-wkEqTerm ξ⊇ (K-β ⊢A ⊢t ok) =
    K-β (defn-wk″ ξ⊇ ⊢A) (defn-wkTerm ξ⊇ ⊢t) ok
  defn-wkEqTerm ξ⊇ ([]-cong-β ⊢l ⊢t eq ok) =
    []-cong-β (defn-wkLevel ξ⊇ ⊢l) (defn-wkTerm ξ⊇ ⊢t) eq ok
  defn-wkEqTerm ξ⊇ (equality-reflection ok ⊢Id ⊢t) =
    equality-reflection ok (defn-wk″ ξ⊇ ⊢Id) (defn-wkTerm ξ⊇ ⊢t)
  defn-wkEqTerm ξ⊇ (Quot-cong ok ⊢l A₁≡A₂ B₁≡B₂) =
    Quot-cong ok (defn-wkLevel ξ⊇ ⊢l) (defn-wkEqTerm ξ⊇ A₁≡A₂)
      (defn-wkEqTerm ξ⊇ B₁≡B₂)
  defn-wkEqTerm ξ⊇ (class-cong ⊢Q t₁≡t₂) =
    class-cong (defn-wk″ ξ⊇ ⊢Q) (defn-wkEqTerm ξ⊇ t₁≡t₂)
  defn-wkEqTerm ξ⊇ (resp-cong ok A₁≡A₂ B₁≡B₂ t₁≡t₂ u₁≡u₂ v₁≡v₂) =
    resp-cong ok (defn-wkEq ξ⊇ A₁≡A₂) (defn-wkEq ξ⊇ B₁≡B₂)
      (defn-wkEqTerm ξ⊇ t₁≡t₂) (defn-wkEqTerm ξ⊇ u₁≡u₂)
      (defn-wkEqTerm ξ⊇ v₁≡v₂)
  defn-wkEqTerm ξ⊇ (set-cong A₁≡A₂ B₁≡B₂ t₁≡t₂ u₁≡u₂ v₁≡v₂ w₁≡w₂) =
    set-cong (defn-wkEq ξ⊇ A₁≡A₂) (defn-wkEq ξ⊇ B₁≡B₂)
      (defn-wkEqTerm ξ⊇ t₁≡t₂) (defn-wkEqTerm ξ⊇ u₁≡u₂)
      (defn-wkEqTerm ξ⊇ v₁≡v₂) (defn-wkEqTerm ξ⊇ w₁≡w₂)
  defn-wkEqTerm
    ξ⊇ (qrec-cong C₁≡C₂ t₁≡t₂ u₁≡u₂ v₁≡v₂ w₁≡w₂) =
    qrec-cong (defn-wkEq ξ⊇ C₁≡C₂) (defn-wkEqTerm ξ⊇ t₁≡t₂)
      (defn-wkEqTerm ξ⊇ u₁≡u₂) (defn-wkEqTerm ξ⊇ v₁≡v₂)
      (defn-wkEqTerm ξ⊇ w₁≡w₂)
  defn-wkEqTerm ξ⊇ (qrec-β ⊢C ⊢t ⊢u ⊢v ⊢w) =
    qrec-β (defn-wk″ ξ⊇ ⊢C) (defn-wkTerm ξ⊇ ⊢t) (defn-wkTerm ξ⊇ ⊢u)
      (defn-wkTerm ξ⊇ ⊢v) (defn-wkTerm ξ⊇ ⊢w)

  defn-wkEqLevel :
    » ∇′ ⊇ ∇ → ∇ » Γ ⊢ l₁ ≡ l₂ ∷Level → ∇′ » Γ ⊢ l₁ ≡ l₂ ∷Level
  defn-wkEqLevel ∇′⊇∇ (term ok l₁≡l₂) =
    term ok (defn-wkEqTerm ∇′⊇∇ l₁≡l₂)
  defn-wkEqLevel ∇′⊇∇ (literal ok ⊢Γ) =
    literal ok (defn-wk′ ∇′⊇∇ ⊢Γ)

opaque

  -- Weakening for definition contexts.

  defn-wk : » ∇′ ⊇ ∇ → ∇ » Γ ⊢[ 𝓙 ] → ∇′ » Γ ⊢[ 𝓙 ]
  defn-wk {𝓙 = [ctxt]}          = defn-wk′
  defn-wk {𝓙 = [ _ type]}       = defn-wk″
  defn-wk {𝓙 = [ _ ≡ _ type]}   = defn-wkEq
  defn-wk {𝓙 = [ _ ∷ _ ]}       = defn-wkTerm
  defn-wk {𝓙 = [ _ ≡ _ ∷ _ ]}   = defn-wkEqTerm
  defn-wk {𝓙 = [ _ ∷Level]}     = defn-wkLevel
  defn-wk {𝓙 = [ _ ≡ _ ∷Level]} = defn-wkEqLevel

------------------------------------------------------------------------
-- Weakening for weakenings

opaque

  -- A definitional weakening lemma for weakenings.

  defn-wkWkʷ : » ∇′ ⊇ ∇ → ∇ » ρ ∷ʷ Δ ⊇ Γ → ∇′ » ρ ∷ʷ Δ ⊇ Γ
  defn-wkWkʷ ξ⊇ ρ = ∷⊇→∷ʷ⊇ (∷ʷ⊇→∷⊇ ρ) (defn-wk ξ⊇ (wf-∷ʷ⊇ ρ))

------------------------------------------------------------------------
-- Weakening for reduction

opaque

  -- A reduction weakening lemma for the definition context.

  defn-wkRedTerm : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ t ⇒ t′ ∷ A → ∇′ » Γ ⊢ t ⇒ t′ ∷ A
  defn-wkRedTerm ξ⊇ (conv t⇒t′ A≡A′) =
    conv (defn-wkRedTerm ξ⊇ t⇒t′) (defn-wk ξ⊇ A≡A′)
  defn-wkRedTerm ξ⊇ (δ-red ⊢Γ α↦t A≡A′ T≡T′) =
    δ-red (defn-wk ξ⊇ ⊢Γ) (there*-↦∷∈ ξ⊇ α↦t) A≡A′ T≡T′
  defn-wkRedTerm ξ⊇ (supᵘ-substˡ l₁⇒l₂ ⊢l₃) =
    supᵘ-substˡ (defn-wkRedTerm ξ⊇ l₁⇒l₂) (defn-wk ξ⊇ ⊢l₃)
  defn-wkRedTerm ξ⊇ (supᵘ-substʳ ⊢l₁ l₂⇒l₃) =
    supᵘ-substʳ (defn-wk ξ⊇ ⊢l₁) (defn-wkRedTerm ξ⊇ l₂⇒l₃)
  defn-wkRedTerm ξ⊇ (supᵘ-zeroˡ ⊢l) =
    supᵘ-zeroˡ (defn-wk ξ⊇ ⊢l)
  defn-wkRedTerm ξ⊇ (supᵘ-zeroʳ ⊢l) =
    supᵘ-zeroʳ (defn-wk ξ⊇ ⊢l)
  defn-wkRedTerm ξ⊇ (supᵘ-sucᵘ ⊢l₁ ⊢l₂) =
    supᵘ-sucᵘ (defn-wk ξ⊇ ⊢l₁) (defn-wk ξ⊇ ⊢l₂)
  defn-wkRedTerm ξ⊇ (lower-subst t⇒u) =
    lower-subst (defn-wkRedTerm ξ⊇ t⇒u)
  defn-wkRedTerm ξ⊇ (Lift-β ⊢A ⊢t) =
    Lift-β (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢t)
  defn-wkRedTerm ξ⊇ (app-subst t⇒t′ ⊢a) =
    app-subst (defn-wkRedTerm ξ⊇ t⇒t′) (defn-wk ξ⊇ ⊢a)
  defn-wkRedTerm ξ⊇ (β-red ⊢A ⊢t ⊢x eq ok) =
    β-red (defn-wk ξ⊇ ⊢A)
          (defn-wk ξ⊇ ⊢t)
          (defn-wk ξ⊇ ⊢x)
          eq ok
  defn-wkRedTerm ξ⊇ (fst-subst ⊢A t⇒t′) =
    fst-subst (defn-wk ξ⊇ ⊢A) (defn-wkRedTerm ξ⊇ t⇒t′)
  defn-wkRedTerm ξ⊇ (snd-subst ⊢A t⇒t′) =
    snd-subst (defn-wk ξ⊇ ⊢A) (defn-wkRedTerm ξ⊇ t⇒t′)
  defn-wkRedTerm ξ⊇ (Σ-β₁ ⊢A ⊢t ⊢t′ eq ok) =
    Σ-β₁ (defn-wk ξ⊇ ⊢A)
         (defn-wk ξ⊇ ⊢t)
         (defn-wk ξ⊇ ⊢t′)
         eq ok
  defn-wkRedTerm ξ⊇ (Σ-β₂ ⊢A ⊢t ⊢t′ eq ok) =
    Σ-β₂ (defn-wk ξ⊇ ⊢A)
         (defn-wk ξ⊇ ⊢t)
         (defn-wk ξ⊇ ⊢t′)
         eq ok
  defn-wkRedTerm ξ⊇ (prodrec-subst ⊢A ⊢a t⇒t′) =
    prodrec-subst (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢a)
      (defn-wkRedTerm ξ⊇ t⇒t′)
  defn-wkRedTerm ξ⊇ (prodrec-β ⊢A ⊢t ⊢t₂ ⊢tᵣ eq) =
    prodrec-β (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢t) (defn-wk ξ⊇ ⊢t₂)
      (defn-wk ξ⊇ ⊢tᵣ) eq
  defn-wkRedTerm ξ⊇ (natrec-subst ⊢t₀ ⊢tₛ t⇒t′) =
    natrec-subst (defn-wk ξ⊇ ⊢t₀)
                 (defn-wk ξ⊇ ⊢tₛ)
                 (defn-wkRedTerm ξ⊇ t⇒t′)
  defn-wkRedTerm ξ⊇ (natrec-zero ⊢t₀ ⊢tₛ) =
    natrec-zero (defn-wk ξ⊇ ⊢t₀) (defn-wk ξ⊇ ⊢tₛ)
  defn-wkRedTerm ξ⊇ (natrec-suc ⊢t₀ ⊢tₛ ⊢t) =
    natrec-suc (defn-wk ξ⊇ ⊢t₀)
               (defn-wk ξ⊇ ⊢tₛ)
               (defn-wk ξ⊇ ⊢t)
  defn-wkRedTerm ξ⊇ (emptyrec-subst ⊢A t⇒t′) =
    emptyrec-subst (defn-wk ξ⊇ ⊢A) (defn-wkRedTerm ξ⊇ t⇒t′)
  defn-wkRedTerm ξ⊇ (unitrec-subst ⊢A ⊢a t⇒t′ no-η) =
    unitrec-subst (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢a)
      (defn-wkRedTerm ξ⊇ t⇒t′) no-η
  defn-wkRedTerm ξ⊇ (unitrec-β ⊢A ⊢t no-η) =
    unitrec-β (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢t) no-η
  defn-wkRedTerm ξ⊇ (unitrec-β-η ⊢A ⊢t ⊢tᵣ η) =
    unitrec-β-η (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢t) (defn-wk ξ⊇ ⊢tᵣ) η
  defn-wkRedTerm ξ⊇ (J-subst ⊢t ⊢A ⊢r ⊢p w⇒w′) =
    J-subst (defn-wk ξ⊇ ⊢t)
            (defn-wk ξ⊇ ⊢A)
            (defn-wk ξ⊇ ⊢r)
            (defn-wk ξ⊇ ⊢p)
            (defn-wkRedTerm ξ⊇ w⇒w′)
  defn-wkRedTerm ξ⊇ (K-subst ⊢A ⊢r t⇒t′ ok) =
    K-subst (defn-wk ξ⊇ ⊢A)
            (defn-wk ξ⊇ ⊢r)
            (defn-wkRedTerm ξ⊇ t⇒t′)
            ok
  defn-wkRedTerm ξ⊇ ([]-cong-subst ⊢l t⇒t′ ok) =
    []-cong-subst (defn-wk ξ⊇ ⊢l) (defn-wkRedTerm ξ⊇ t⇒t′) ok
  defn-wkRedTerm ξ⊇ (J-β ⊢t ⊢t′ t≡t′ ⊢A A≡ ⊢tᵣ) =
    J-β (defn-wk ξ⊇ ⊢t)
        (defn-wk ξ⊇ ⊢t′)
        (defn-wk ξ⊇ t≡t′)
        (defn-wk ξ⊇ ⊢A)
        (defn-wk ξ⊇ A≡)
        (defn-wk ξ⊇ ⊢tᵣ)
  defn-wkRedTerm ξ⊇ (K-β ⊢A ⊢t ok) =
    K-β (defn-wk ξ⊇ ⊢A) (defn-wk ξ⊇ ⊢t) ok
  defn-wkRedTerm ξ⊇ ([]-cong-β ⊢l t≡t′ ok) =
    []-cong-β (defn-wk ξ⊇ ⊢l) (defn-wk ξ⊇ t≡t′) ok
  defn-wkRedTerm ξ⊇ (resp-η ok ⊢Q ⊢t ⊢u ⊢v) =
    resp-η ok (defn-wk ξ⊇ ⊢Q) (defn-wk ξ⊇ ⊢t) (defn-wk ξ⊇ ⊢u)
      (defn-wk ξ⊇ ⊢v)
  defn-wkRedTerm ξ⊇ (set-η ok ⊢t ⊢u ⊢v ⊢w) =
    set-η ok (defn-wk ξ⊇ ⊢t) (defn-wk ξ⊇ ⊢u) (defn-wk ξ⊇ ⊢v)
      (defn-wk ξ⊇ ⊢w)
  defn-wkRedTerm ξ⊇ (qrec-subst ⊢C ⊢t ⊢u ⊢v w₁⇒w₂) =
    qrec-subst (defn-wk ξ⊇ ⊢C) (defn-wk ξ⊇ ⊢t) (defn-wk ξ⊇ ⊢u)
      (defn-wk ξ⊇ ⊢v) (defn-wkRedTerm ξ⊇ w₁⇒w₂)
  defn-wkRedTerm ξ⊇ (qrec-β ⊢C ⊢t ⊢u ⊢v ⊢w) =
    qrec-β (defn-wk ξ⊇ ⊢C) (defn-wk ξ⊇ ⊢t) (defn-wk ξ⊇ ⊢u)
      (defn-wk ξ⊇ ⊢v) (defn-wk ξ⊇ ⊢w)

opaque

  -- A reduction weakening lemma for the definition context.

  defn-wkRed : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ A ⇒ A′ → ∇′ » Γ ⊢ A ⇒ A′
  defn-wkRed ξ⊇ (univ A⇒A′) = univ (defn-wkRedTerm ξ⊇ A⇒A′)

opaque

  -- A multi-step reduction weakening lemma for the definition context.

  defn-wkRed* : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ A ⇒* A′ → ∇′ » Γ ⊢ A ⇒* A′
  defn-wkRed* ξ⊇ (id ⊢A)       = id (defn-wk ξ⊇ ⊢A)
  defn-wkRed* ξ⊇ (A⇒X ⇨ X⇒*A′) = defn-wkRed ξ⊇ A⇒X ⇨ defn-wkRed* ξ⊇ X⇒*A′

opaque

  -- A multi-step reduction weakening lemma for the definition context.

  defn-wkRed*Term :
    » ∇′ ⊇ ∇ → ∇ » Γ ⊢ t ⇒* t′ ∷ A → ∇′ » Γ ⊢ t ⇒* t′ ∷ A
  defn-wkRed*Term ξ⊇ (id ⊢t)       = id (defn-wk ξ⊇ ⊢t)
  defn-wkRed*Term ξ⊇ (t⇒x ⇨ x⇒*t′) =
    defn-wkRedTerm ξ⊇ t⇒x ⇨ defn-wkRed*Term ξ⊇ x⇒*t′

------------------------------------------------------------------------
-- Weakening for WHNF properties

opaque

  -- A neutral term weakening lemma for the definition context.

  defn-wkNeutral : » ∇′ ⊇ ∇ → Neutral V ∇ t → Neutral V ∇′ t
  defn-wkNeutral ξ⊇ (defn α↦⊘)     = defn (there*-↦⊘∈ ξ⊇ α↦⊘)
  defn-wkNeutral ξ⊇ (var ok x)     = var ok x
  defn-wkNeutral ξ⊇ (supᵘˡₙ b)     = supᵘˡₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (supᵘʳₙ b)     = supᵘʳₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (lowerₙ b)     = lowerₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (∘ₙ b)         = ∘ₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (fstₙ b)       = fstₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (sndₙ b)       = sndₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (natrecₙ b)    = natrecₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (prodrecₙ b)   = prodrecₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (emptyrecₙ b)  = emptyrecₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (unitrecₙ x b) = unitrecₙ x (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (Jₙ b)         = Jₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ (Kₙ b)         = Kₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral ξ⊇ ([]-congₙ b)   = []-congₙ (defn-wkNeutral ξ⊇ b)
  defn-wkNeutral _  (resp ok)      = resp ok
  defn-wkNeutral _  (set ok)       = set ok
  defn-wkNeutral ξ⊇ (qrec n)       = qrec (defn-wkNeutral ξ⊇ n)

opaque

  -- A variant of defn-wkNeutral for Neutralᵃ.

  defn-wkNeutralᵃ : » ∇′ ⊇ ∇ → Neutralᵃ V ∇ t → Neutralᵃ V ∇′ t
  defn-wkNeutralᵃ ∇′⊇∇ (ne t-n t-nn) =
    ne (defn-wkNeutral ∇′⊇∇ t-n) t-nn

opaque

  -- A WHNF weakening lemma for the definition context.

  defn-wkWhnf : » ∇′ ⊇ ∇ → Whnf ∇ t → Whnf ∇′ t
  defn-wkWhnf _  Levelₙ = Levelₙ
  defn-wkWhnf ξ⊇ Uₙ     = Uₙ
  defn-wkWhnf _  Liftₙ  = Liftₙ
  defn-wkWhnf ξ⊇ ΠΣₙ    = ΠΣₙ
  defn-wkWhnf ξ⊇ ℕₙ     = ℕₙ
  defn-wkWhnf ξ⊇ Unitₙ  = Unitₙ
  defn-wkWhnf ξ⊇ Emptyₙ = Emptyₙ
  defn-wkWhnf ξ⊇ Idₙ    = Idₙ
  defn-wkWhnf _  zeroᵘₙ = zeroᵘₙ
  defn-wkWhnf _  sucᵘₙ  = sucᵘₙ
  defn-wkWhnf _  liftₙ  = liftₙ
  defn-wkWhnf ξ⊇ lamₙ   = lamₙ
  defn-wkWhnf ξ⊇ zeroₙ  = zeroₙ
  defn-wkWhnf ξ⊇ sucₙ   = sucₙ
  defn-wkWhnf ξ⊇ starₙ  = starₙ
  defn-wkWhnf ξ⊇ prodₙ  = prodₙ
  defn-wkWhnf ξ⊇ rflₙ   = rflₙ
  defn-wkWhnf _  Quot   = Quot
  defn-wkWhnf _  class  = class
  defn-wkWhnf ξ⊇ (ne n) = ne (defn-wkNeutral ξ⊇ n)

opaque

  -- A WHNF view weakening lemma for the definition context.

  defn-wkNatural : » ∇′ ⊇ ∇ → Natural V ∇ t → Natural V ∇′ t
  defn-wkNatural ξ⊇ sucₙ   = sucₙ
  defn-wkNatural ξ⊇ zeroₙ  = zeroₙ
  defn-wkNatural ξ⊇ (ne n) = ne (defn-wkNeutral ξ⊇ n)

opaque

  -- A WHNF view weakening lemma for the definition context.

  defn-wkType : » ∇′ ⊇ ∇ → Type V ∇ t → Type V ∇′ t
  defn-wkType _  Levelₙ = Levelₙ
  defn-wkType ξ⊇ Uₙ     = Uₙ
  defn-wkType _  Liftₙ  = Liftₙ
  defn-wkType ξ⊇ ΠΣₙ    = ΠΣₙ
  defn-wkType ξ⊇ ℕₙ     = ℕₙ
  defn-wkType ξ⊇ Emptyₙ = Emptyₙ
  defn-wkType ξ⊇ Unitₙ  = Unitₙ
  defn-wkType ξ⊇ Idₙ    = Idₙ
  defn-wkType _  Quot   = Quot
  defn-wkType ξ⊇ (ne n) = ne (defn-wkNeutral ξ⊇ n)

opaque

  -- A WHNF view weakening lemma for the definition context.

  defn-wkFunction : » ∇′ ⊇ ∇ → Function V ∇ t → Function V ∇′ t
  defn-wkFunction ξ⊇ lamₙ   = lamₙ
  defn-wkFunction ξ⊇ (ne n) = ne (defn-wkNeutral ξ⊇ n)

opaque

  -- A variant of defn-wkFunction for Functionᵃ.

  defn-wkFunctionᵃ : » ∇′ ⊇ ∇ → Functionᵃ V ∇ t → Functionᵃ V ∇′ t
  defn-wkFunctionᵃ _    lamₙ   = lamₙ
  defn-wkFunctionᵃ ∇′⊇∇ (ne n) = ne (defn-wkNeutralᵃ ∇′⊇∇ n)

opaque

  -- A WHNF view weakening lemma for the definition context.

  defn-wkProduct : » ∇′ ⊇ ∇ → Product V ∇ t → Product V ∇′ t
  defn-wkProduct ξ⊇ prodₙ  = prodₙ
  defn-wkProduct ξ⊇ (ne n) = ne (defn-wkNeutral ξ⊇ n)

opaque

  -- A variant of defn-wkProduct for Productᵃ.

  defn-wkProductᵃ : » ∇′ ⊇ ∇ → Productᵃ V ∇ t → Productᵃ V ∇′ t
  defn-wkProductᵃ _    prodₙ  = prodₙ
  defn-wkProductᵃ ∇′⊇∇ (ne n) = ne (defn-wkNeutralᵃ ∇′⊇∇ n)

opaque

  -- A WHNF view weakening lemma for the definition context.

  defn-wkIdentity : » ∇′ ⊇ ∇ → Identity V ∇ t → Identity V ∇′ t
  defn-wkIdentity ξ⊇ rflₙ   = rflₙ
  defn-wkIdentity ξ⊇ (ne n) = ne (defn-wkNeutral ξ⊇ n)

opaque

  -- A variant of defn-wkIdentity for Identityᵃ.

  defn-wkIdentityᵃ : » ∇′ ⊇ ∇ → Identityᵃ V ∇ t → Identityᵃ V ∇′ t
  defn-wkIdentityᵃ _    rflₙ   = rflₙ
  defn-wkIdentityᵃ ∇′⊇∇ (ne n) = ne (defn-wkNeutralᵃ ∇′⊇∇ n)

opaque

  -- A normalization weakening lemma for the definition context.

  defn-wkRed↘ : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ A ↘ A′ → ∇′ » Γ ⊢ A ↘ A′
  defn-wkRed↘ ξ⊇ (A⇒*A′ , w) = defn-wkRed* ξ⊇ A⇒*A′ , defn-wkWhnf ξ⊇ w

opaque

  -- A normalization weakening lemma for the definition context.

  defn-wkRed↘Term : » ∇′ ⊇ ∇ → ∇ » Γ ⊢ t ↘ t′ ∷ A → ∇′ » Γ ⊢ t ↘ t′ ∷ A
  defn-wkRed↘Term ξ⊇ (t⇒*t′ , w) = defn-wkRed*Term ξ⊇ t⇒*t′ , defn-wkWhnf ξ⊇ w