------------------------------------------------------------------------
-- A variant of Definition.Typed.Stability with fewer dependencies
------------------------------------------------------------------------

{-# OPTIONS --backtracking-instance-search #-}

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

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

open import Definition.Typed R
open import Definition.Typed.Inversion.Primitive R
open import Definition.Typed.Properties.Admissible.Level.Primitive R
open import Definition.Typed.Properties.Admissible.Var R
open import Definition.Typed.Properties.Definition.Primitive R
open import Definition.Typed.Properties.Well-formed R
open import Definition.Typed.Size R
open import Definition.Typed.Weakening R
open import Definition.Untyped M hiding (wk)
open import Definition.Untyped.Quotient 𝕄

open import Tools.Fin
open import Tools.Function
open import Tools.Nat
open import Tools.Product as Σ
import Tools.PropositionalEquality as PE
open import Tools.Size
open import Tools.Size.Instances

private variable
  m n       : Nat
  ∇         : DCon (Term ) _
  x         : Fin _
  Γ Δ Η     : Con Term _
  𝓙         : Judgement _
  A B C t u : Term _
  l l₁ l₂   : Lvl _
  σ σ₁ σ₂   : Subst _ _
  s s₂      : Size

-- Equality of contexts.

infix  _∙⟨_∣_⟩

data _»⊢_≡_ : (∇ : DCon (Term ) m) (_ _ : Con Term n) → Set a where
  ε       : » ∇ → ∇ »⊢ ε ≡ ε
  _∙⟨_∣_⟩ : ∇ »⊢ Γ ≡ Δ → ∇ » Δ ⊢ B → ∇ » Δ ⊢ A ≡ B → ∇ »⊢ Γ ∙ A ≡ Δ ∙ B

opaque

  -- A variant of _∙⟨_∣_⟩.

  infix  _∙⟨_⟩

  _∙⟨_⟩ : ∇ »⊢ Γ ≡ Δ → ∇ » Δ ⊢ A → ∇ »⊢ Γ ∙ A ≡ Δ ∙ A
  Γ≡Δ ∙⟨ ⊢A ⟩ = Γ≡Δ ∙⟨ ⊢A ∣ refl ⊢A ⟩

opaque

  -- A well-formedness lemma for ⊢_≡_.

  wf-⊢≡ʳ : ∇ »⊢ Γ ≡ Δ → ∇ »⊢ Δ
  wf-⊢≡ʳ (ε »∇)          = ε »∇
  wf-⊢≡ʳ (_ ∙⟨ ⊢B ∣ _ ⟩) = ∙ ⊢B

opaque

  -- Reflexivity for ⊢_≡_.

  reflConEq : ∇ »⊢ Γ → ∇ »⊢ Γ ≡ Γ
  reflConEq (ε »∇) = ε »∇
  reflConEq (∙ ⊢A) = reflConEq (wf ⊢A) ∙⟨ ⊢A ⟩

opaque

  -- A variant of _∙⟨_∣_⟩.

  refl-∙⟨_∣_⟩ : ∇ » Γ ⊢ B → ∇ » Γ ⊢ A ≡ B → ∇ »⊢ Γ ∙ A ≡ Γ ∙ B
  refl-∙⟨ ⊢B ∣ A≡B ⟩ = reflConEq (wf ⊢B) ∙⟨ ⊢B ∣ A≡B ⟩

opaque

  -- If ∇ »⊢ Γ ∙ A ≡ Δ ∙ B holds, then ∇ »⊢ Γ ≡ Δ also holds.

  ⊢∙≡∙→⊢≡ : ∇ »⊢ Γ ∙ A ≡ Δ ∙ B → ∇ »⊢ Γ ≡ Δ
  ⊢∙≡∙→⊢≡ (Γ≡Δ ∙⟨ _ ∣ _ ⟩) = Γ≡Δ

opaque

  -- A glassification lemma for _»⊢_≡_.

  glassify-»⊢≡ : ∇ »⊢ Γ ≡ Δ → glassify ∇ »⊢ Γ ≡ Δ
  glassify-»⊢≡ (ε »∇) =
    ε (glassify-» »∇)
  glassify-»⊢≡ (Γ≡Δ ∙⟨ ⊢B ∣ A≡B ⟩) =
    glassify-»⊢≡ Γ≡Δ ∙⟨ glassify-⊢ ⊢B ∣ glassify-⊢ A≡B ⟩

opaque

  -- Stability for _∷_∈_.

  stability-⊢∈ :
    ∇ »⊢ Γ ≡ Δ → x ∷ A ∈ Γ →
    ∃ λ B → ∇ » Δ ⊢ A ≡ B × x ∷ B ∈ Δ
  stability-⊢∈ (ε ⊢ε)              ()
  stability-⊢∈ (Γ≡Δ ∙⟨ ⊢B ∣ A≡B ⟩) here =
    _ , wk₁ ⊢B A≡B , here
  stability-⊢∈ (Γ≡Δ ∙⟨ ⊢B ∣ _ ⟩) (there x∈) =
    Σ.map wk1 (Σ.map (wk₁ ⊢B) there) $
    stability-⊢∈ Γ≡Δ x∈

private

  -- Below several properties are proved simultaneously using
  -- well-founded induction. The properties are collected in the
  -- record type P.

  record P (s : Size) : Set a where
    no-eta-equality
    field
      stability-⊢ :
        ∇ »⊢ Γ ≡ Δ →
        (⊢A : ∇ » Γ ⊢ A) →
        size ⊢A PE.≡ s →
        ∇ » Δ ⊢ A
      stability-⊢≡ :
        ∇ »⊢ Γ ≡ Δ →
        (A≡B : ∇ » Γ ⊢ A ≡ B) →
        size A≡B PE.≡ s →
        ∇ » Δ ⊢ A ≡ B
      stability-⊢∷ :
        ∇ »⊢ Γ ≡ Δ →
        (⊢t : ∇ » Γ ⊢ t ∷ A) →
        size ⊢t PE.≡ s →
        ∇ » Δ ⊢ t ∷ A
      stability-⊢∷L :
        ∇ »⊢ Γ ≡ Δ →
        (⊢l : ∇ » Γ ⊢ l ∷Level) →
        size ⊢l PE.≡ s →
        ∇ » Δ ⊢ l ∷Level
      stability-⊢≡∷ :
        ∇ »⊢ Γ ≡ Δ →
        (t≡u : ∇ » Γ ⊢ t ≡ u ∷ A) →
        size t≡u PE.≡ s →
        ∇ » Δ ⊢ t ≡ u ∷ A
      stability-⊢≡∷L :
        ∇ »⊢ Γ ≡ Δ →
        (l₁≡l₂ : ∇ » Γ ⊢ l₁ ≡ l₂ ∷Level) →
        size l₁≡l₂ PE.≡ s →
        ∇ » Δ ⊢ l₁ ≡ l₂ ∷Level

-- Variants of the fields of P, along with some lemmas.

private module Variants (hyp : ∀ {s₁} → s₁ <ˢ s₂ → P s₁) where

  opaque

    -- Variants of the fields of P.

    stability-⊢ :
      ∇ »⊢ Γ ≡ Δ →
      (⊢A : ∇ » Γ ⊢ A)
      ⦃ lt : size ⊢A <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ A
    stability-⊢ Γ≡Δ ⊢A ⦃ lt ⦄ = P.stability-⊢ (hyp lt) Γ≡Δ ⊢A PE.refl

    stability-⊢≡ :
      ∇ »⊢ Γ ≡ Δ →
      (A≡B : ∇ » Γ ⊢ A ≡ B)
      ⦃ lt : size A≡B <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ A ≡ B
    stability-⊢≡ Γ≡Δ A≡B ⦃ lt ⦄ =
      P.stability-⊢≡ (hyp lt) Γ≡Δ A≡B PE.refl

    stability-⊢∷ :
      ∇ »⊢ Γ ≡ Δ →
      (⊢t : ∇ » Γ ⊢ t ∷ A)
      ⦃ lt : size ⊢t <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ t ∷ A
    stability-⊢∷ Γ≡Δ ⊢t ⦃ lt ⦄ = P.stability-⊢∷ (hyp lt) Γ≡Δ ⊢t PE.refl

    stability-⊢∷L :
      ∇ »⊢ Γ ≡ Δ →
      (⊢l : ∇ » Γ ⊢ l ∷Level)
      ⦃ lt : size ⊢l <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ l ∷Level
    stability-⊢∷L Γ≡Δ ⊢l ⦃ lt ⦄ =
      P.stability-⊢∷L (hyp lt) Γ≡Δ ⊢l PE.refl

    stability-⊢≡∷ :
      ∇ »⊢ Γ ≡ Δ →
      (t≡u : ∇ » Γ ⊢ t ≡ u ∷ A)
      ⦃ lt : size t≡u <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ t ≡ u ∷ A
    stability-⊢≡∷ Γ≡Δ t≡u ⦃ lt ⦄ =
      P.stability-⊢≡∷ (hyp lt) Γ≡Δ t≡u PE.refl

    stability-⊢≡∷L :
      ∇ »⊢ Γ ≡ Δ →
      (l₁≡l₂ : ∇ » Γ ⊢ l₁ ≡ l₂ ∷Level)
      ⦃ lt : size l₁≡l₂ <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ l₁ ≡ l₂ ∷Level
    stability-⊢≡∷L Γ≡Δ l₁≡l₂ ⦃ lt ⦄ =
      P.stability-⊢≡∷L (hyp lt) Γ≡Δ l₁≡l₂ PE.refl

  opaque

    -- Some variants of the variants.

    stability-⊢-<ˢ :
      ∇ »⊢ Γ ≡ Δ →
      (∃ λ (⊢A : ∇ » Γ ⊢ A) → size ⊢A <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ A
    stability-⊢-<ˢ Γ≡Δ (⊢A , A<) =
      stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄

    stability-⊢∷-<ˢ :
      ∇ »⊢ Γ ≡ Δ →
      (∃ λ (⊢t : ∇ » Γ ⊢ t ∷ A) → size ⊢t <ˢ s) →
      ⦃ lt : s <ˢ s₂ ⦄ →
      ∇ » Δ ⊢ t ∷ A
    stability-⊢∷-<ˢ Γ≡Δ (⊢t , t<) =
      stability-⊢∷ Γ≡Δ ⊢t ⦃ lt = <ˢ-trans t< ! ⦄

  opaque
    unfolding Quot-rel-Con Resp-Con

    -- A lemma related to Resp-Con.

    stability-Resp-Con :
      ∇ »⊢ Γ ≡ Δ →
      (⊢R : ∇ »⊢ Resp-Con Γ A B)
      ⦃ lt : size ⊢R <ˢ s₂ ⦄ →
      ∇ »⊢ Resp-Con Γ A B ≡ Resp-Con Δ A B
    stability-Resp-Con Γ≡Δ ⊢R =
      let _ , ⊢A , ⊢wk1-A , ⊢B = ∙∙∙⊢→⊢-<ˢ ⊢R
          Eq₁                  = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A ⟩
          Eq₂                  = Eq₁ ∙⟨ stability-⊢-<ˢ Eq₁ ⊢wk1-A ⟩
      in
      Eq₂ ∙⟨ stability-⊢-<ˢ Eq₂ ⊢B ⟩

  opaque
    unfolding Is-set-Con

    -- A lemma related to Is-set-Con.

    stability-Is-set-Con :
      ∇ »⊢ Γ ≡ Δ →
      (⊢S : ∇ »⊢ Is-set-Con Γ A B C)
      ⦃ lt : size ⊢S <ˢ s₂ ⦄ →
      ∇ »⊢ Is-set-Con Γ A B C ≡ Is-set-Con Δ A B C
    stability-Is-set-Con Γ≡Δ ⊢S =
      let _ , ⊢Q , ⊢C , ⊢wk1-C , ⊢Id-1-0 , ⊢Id-2-1 =
            ∙∙∙∙∙⊢→⊢-<ˢ ⊢S
          Eq₁ = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢Q ⟩
          Eq₂ = Eq₁ ∙⟨ stability-⊢-<ˢ Eq₁ ⊢C ⟩
          Eq₃ = Eq₂ ∙⟨ stability-⊢-<ˢ Eq₂ ⊢wk1-C ⟩
          Eq₄ = Eq₃ ∙⟨ stability-⊢-<ˢ Eq₃ ⊢Id-1-0 ⟩
      in
      Eq₄ ∙⟨ stability-⊢-<ˢ Eq₄ ⊢Id-2-1 ⟩

-- The type P s is inhabited for every s.

private module Inhabited where

  opaque
    unfolding Quot-rel-Con size

    -- Stability for _⊢_.

    stability-⊢′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      ∇ »⊢ Γ ≡ Δ →
      (⊢A : ∇ » Γ ⊢ A) →
      size ⊢A PE.≡ s₂ →
      ∇ » Δ ⊢ A
    stability-⊢′ hyp Γ≡Δ = let open Variants hyp in λ where
      (Levelⱼ ok _) _ →
        Levelⱼ ok (wf-⊢≡ʳ Γ≡Δ)
      (univ ⊢A) PE.refl →
        univ (stability-⊢∷ Γ≡Δ ⊢A)
      (Liftⱼ ⊢l ⊢A) PE.refl →
        Liftⱼ (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢ Γ≡Δ ⊢A)
      (ΠΣⱼ ⊢B ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        ΠΣⱼ (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) ok
      (Idⱼ ⊢A ⊢t ⊢u) PE.refl →
        Idⱼ (stability-⊢ Γ≡Δ ⊢A) (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ Γ≡Δ ⊢u)
      (Quot ok ⊢B) PE.refl →
        let _ , ⊢A , ⊢wk1-A = ∙∙⊢→⊢-<ˢ ⊢B
            ΓA≡ΔA           = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A ⟩
        in
        Quot ok
          (stability-⊢ (ΓA≡ΔA ∙⟨ stability-⊢-<ˢ ΓA≡ΔA ⊢wk1-A ⟩) ⊢B)

  opaque
    unfolding Quot-rel-Con size

    -- Stability for _⊢_≡_.

    stability-⊢≡′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      ∇ »⊢ Γ ≡ Δ →
      (A≡B : ∇ » Γ ⊢ A ≡ B) →
      size A≡B PE.≡ s₂ →
      ∇ » Δ ⊢ A ≡ B
    stability-⊢≡′ hyp Γ≡Δ = let open Variants hyp in λ where
      (refl ⊢A) PE.refl →
        refl (stability-⊢ Γ≡Δ ⊢A)
      (sym B≡A) PE.refl →
        sym (stability-⊢≡ Γ≡Δ B≡A)
      (trans A≡B B≡C) PE.refl →
        trans (stability-⊢≡ Γ≡Δ A≡B) (stability-⊢≡ Γ≡Δ B≡C)
      (univ A≡B) PE.refl →
        univ (stability-⊢≡∷ Γ≡Δ A≡B)
      (U-cong l₁≡l₂) PE.refl →
        U-cong (stability-⊢≡∷ Γ≡Δ l₁≡l₂)
      (Lift-cong l₁≡l₂ A≡B) PE.refl →
        Lift-cong (stability-⊢≡∷L Γ≡Δ l₁≡l₂) (stability-⊢≡ Γ≡Δ A≡B)
      (ΠΣ-cong A₁≡B₁ A₂≡B₂ ok) PE.refl →
        let _ , (⊢A₁ , A₁<) = ∙⊢→⊢-<ˢ A₂≡B₂
            ⊢A₁′            = stability-⊢ Γ≡Δ ⊢A₁
                                ⦃ lt = <ˢ-trans A₁< ! ⦄
        in
        ΠΣ-cong (stability-⊢≡ Γ≡Δ A₁≡B₁)
          (stability-⊢≡ (Γ≡Δ ∙⟨ ⊢A₁′ ⟩) A₂≡B₂) ok
      (Id-cong A≡B t₁≡u₁ t₂≡u₂) PE.refl →
        Id-cong (stability-⊢≡ Γ≡Δ A≡B) (stability-⊢≡∷ Γ≡Δ t₁≡u₁)
          (stability-⊢≡∷ Γ≡Δ t₂≡u₂)
      (Quot-cong {A₁} ok A₁≡A₂ B₁≡B₂) PE.refl →
        let _ , ⊢A₁ , ⊢wk1-A₁ = ∙∙⊢→⊢-<ˢ B₁≡B₂
            ΓA₁≡ΔA₁           = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A₁ ⟩
        in
        Quot-cong ok (stability-⊢≡ Γ≡Δ A₁≡A₂)
          (stability-⊢≡
             (ΓA₁≡ΔA₁ ∙⟨ stability-⊢-<ˢ ΓA₁≡ΔA₁ ⊢wk1-A₁ ⟩) B₁≡B₂)

  opaque
    unfolding Quot-rel-Con size

    -- Stability for _⊢_∷_.

    stability-⊢∷′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      ∇ »⊢ Γ ≡ Δ →
      (⊢t : ∇ » Γ ⊢ t ∷ A) →
      size ⊢t PE.≡ s₂ →
      ∇ » Δ ⊢ t ∷ A
    stability-⊢∷′ hyp Γ≡Δ = let open Variants hyp in λ where
      (conv ⊢t B≡A) PE.refl →
        conv (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢≡ Γ≡Δ B≡A)
      (var _ x∈Γ) _ →
        let _ , A≡B , x∈Δ = stability-⊢∈ Γ≡Δ x∈Γ in
        conv (var (wf-⊢≡ʳ Γ≡Δ) x∈Δ) (sym A≡B)
      (defn ⊢Γ α↦t A≡A′) PE.refl →
        defn (wf-⊢≡ʳ Γ≡Δ) α↦t A≡A′
      (Levelⱼ _ ok) _ →
        Levelⱼ (wf-⊢≡ʳ Γ≡Δ) ok
      (zeroᵘⱼ ok _) _ →
        zeroᵘⱼ ok (wf-⊢≡ʳ Γ≡Δ)
      (sucᵘⱼ ⊢t) PE.refl →
        sucᵘⱼ (stability-⊢∷ Γ≡Δ ⊢t)
      (supᵘⱼ ⊢t ⊢u) PE.refl →
        supᵘⱼ (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢∷ Γ≡Δ ⊢u)
      (Uⱼ ⊢l) PE.refl →
        Uⱼ (stability-⊢∷L Γ≡Δ ⊢l)
      (Liftⱼ ⊢l₁ ⊢l₂ ⊢A) PE.refl →
        Liftⱼ (stability-⊢∷L Γ≡Δ ⊢l₁) (stability-⊢∷L Γ≡Δ ⊢l₂)
          (stability-⊢∷ Γ≡Δ ⊢A)
      (liftⱼ ⊢l ⊢A ⊢t) PE.refl →
        liftⱼ (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢ Γ≡Δ ⊢A)
          (stability-⊢∷ Γ≡Δ ⊢t)
      (lowerⱼ x) PE.refl →
        lowerⱼ (stability-⊢∷ Γ≡Δ x)
      (ΠΣⱼ l ⊢A ⊢B ok) PE.refl →
        let ⊢A′ = stability-⊢∷ Γ≡Δ ⊢A in
        ΠΣⱼ (stability-⊢∷L Γ≡Δ l) ⊢A′
          (stability-⊢∷ (Γ≡Δ ∙⟨ univ ⊢A′ ⟩) ⊢B) ok
      (lamⱼ ⊢B ⊢t ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢t
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
            Γ∙A≡Δ∙A       = Γ≡Δ ∙⟨ ⊢A′ ⟩
        in
        lamⱼ (stability-⊢ Γ∙A≡Δ∙A ⊢B) (stability-⊢∷ Γ∙A≡Δ∙A ⊢t) ok
      (⊢t ∘ⱼ ⊢u) PE.refl →
        stability-⊢∷ Γ≡Δ ⊢t ∘ⱼ stability-⊢∷ Γ≡Δ ⊢u
      (prodⱼ ⊢B ⊢t ⊢u ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        prodⱼ (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ Γ≡Δ ⊢u) ok
      (fstⱼ ⊢B ⊢t) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        fstⱼ (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) (stability-⊢∷ Γ≡Δ ⊢t)
      (sndⱼ ⊢B ⊢t) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        sndⱼ (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) (stability-⊢∷ Γ≡Δ ⊢t)
      (prodrecⱼ ⊢C ⊢t ⊢u) PE.refl →
        let _ , _ , ok                = inversion-ΠΣ (⊢∙→⊢ (wf ⊢C))
            _ , (⊢A , A<) , (⊢B , B<) = ∙∙⊢→⊢-<ˢ ⊢u
            ⊢A′                       = stability-⊢ Γ≡Δ ⊢A
                                          ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢B′                       = stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B
                                          ⦃ lt = <ˢ-trans B< ! ⦄
        in
        prodrecⱼ (stability-⊢ (Γ≡Δ ∙⟨ ΠΣⱼ ⊢B′ ok ⟩) ⊢C)
          (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ (Γ≡Δ ∙⟨ ⊢A′ ⟩ ∙⟨ ⊢B′ ⟩) ⊢u)
      (Emptyⱼ _) _ →
        Emptyⱼ (wf-⊢≡ʳ Γ≡Δ)
      (emptyrecⱼ ⊢A ⊢t) PE.refl →
        emptyrecⱼ (stability-⊢ Γ≡Δ ⊢A) (stability-⊢∷ Γ≡Δ ⊢t)
      (Unitⱼ ⊢Γ ok) PE.refl →
        Unitⱼ (wf-⊢≡ʳ Γ≡Δ) ok
      (starⱼ ⊢Γ ok) PE.refl →
        starⱼ (wf-⊢≡ʳ Γ≡Δ) ok
      (unitrecⱼ ⊢A ⊢t ⊢u) PE.refl →
        let ok = inversion-Unit (⊢∙→⊢ (wf ⊢A)) in
        unitrecⱼ
          (stability-⊢ (Γ≡Δ ∙⟨ univ (Unitⱼ (wf-⊢≡ʳ Γ≡Δ) ok) ⟩) ⊢A)
          (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢∷ Γ≡Δ ⊢u)
      (ℕⱼ _) _ →
        ℕⱼ (wf-⊢≡ʳ Γ≡Δ)
      (zeroⱼ _) _ →
        zeroⱼ (wf-⊢≡ʳ Γ≡Δ)
      (sucⱼ ⊢t) PE.refl →
        sucⱼ (stability-⊢∷ Γ≡Δ ⊢t)
      (natrecⱼ ⊢t ⊢u ⊢v) PE.refl →
        let ⊢ℕ            = univ (ℕⱼ (wf-⊢≡ʳ Γ≡Δ))
            _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢u
            ⊢A′           = stability-⊢ (Γ≡Δ ∙⟨ ⊢ℕ ⟩) ⊢A
                              ⦃ lt = <ˢ-trans A< ! ⦄
        in
        natrecⱼ (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ (Γ≡Δ ∙⟨ ⊢ℕ ⟩ ∙⟨ ⊢A′ ⟩) ⊢u) (stability-⊢∷ Γ≡Δ ⊢v)
      (Idⱼ ⊢A ⊢t ⊢u) PE.refl →
        Idⱼ (stability-⊢∷ Γ≡Δ ⊢A) (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ Γ≡Δ ⊢u)
      (rflⱼ ⊢t) PE.refl →
        rflⱼ (stability-⊢∷ Γ≡Δ ⊢t)
      (Jⱼ ⊢t ⊢B ⊢u ⊢v ⊢w) PE.refl →
        let _ , (⊢A , A<) , _ = ∙∙⊢→⊢-<ˢ ⊢B
            ⊢A′               = stability-⊢ Γ≡Δ ⊢A
                                  ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢t′               = stability-⊢∷ Γ≡Δ ⊢t
        in
        Jⱼ ⊢t′
          (stability-⊢
             (Γ≡Δ
                ∙⟨ ⊢A′ ⟩
                ∙⟨ Idⱼ (wk₁ ⊢A′ ⊢A′) (wk₁ ⊢A′ ⊢t′) (var₀ ⊢A′) ⟩)
             ⊢B)
          (stability-⊢∷ Γ≡Δ ⊢u) (stability-⊢∷ Γ≡Δ ⊢v)
          (stability-⊢∷ Γ≡Δ ⊢w)
      (Kⱼ ⊢B ⊢u ⊢v ok) PE.refl →
        let _ , ⊢Id                   = ∙⊢→⊢-<ˢ ⊢B
            (⊢A , A<) , (⊢t , t<) , _ = inversion-Id-⊢-<ˢ ⊢Id
            ⊢A′                       = stability-⊢ Γ≡Δ ⊢A
                                          ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢t′                       = stability-⊢∷ Γ≡Δ ⊢t
                                          ⦃ lt = <ˢ-trans t< ! ⦄
        in
        Kⱼ (stability-⊢ (Γ≡Δ ∙⟨ Idⱼ ⊢A′ ⊢t′ ⊢t′ ⟩) ⊢B)
          (stability-⊢∷ Γ≡Δ ⊢u) (stability-⊢∷ Γ≡Δ ⊢v) ok
      ([]-congⱼ ⊢l ⊢A ⊢t ⊢u ⊢v ok) PE.refl →
        []-congⱼ (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢ Γ≡Δ ⊢A)
          (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢∷ Γ≡Δ ⊢u)
          (stability-⊢∷ Γ≡Δ ⊢v) ok
      (Quot ok ⊢l ⊢A ⊢B) PE.refl →
        let _ , ⊢wk1-A = ∙⊢→⊢-<ˢ ⊢B
            ΓA≡ΔA      = Γ≡Δ ∙⟨ univ (stability-⊢∷ Γ≡Δ ⊢A) ⟩
        in
        Quot ok (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢∷ Γ≡Δ ⊢A)
          (stability-⊢∷ (ΓA≡ΔA ∙⟨ stability-⊢-<ˢ ΓA≡ΔA ⊢wk1-A ⟩) ⊢B)
      (class ⊢Q ⊢t) PE.refl →
        class (stability-⊢ Γ≡Δ ⊢Q) (stability-⊢∷ Γ≡Δ ⊢t)
      (resp {B} ⊢Q ⊢t ⊢u ⊢v) PE.refl →
        resp (stability-⊢ Γ≡Δ ⊢Q) (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ Γ≡Δ ⊢u) (stability-⊢∷ Γ≡Δ ⊢v)
      (set ⊢Q ⊢t ⊢u ⊢v ⊢w) PE.refl →
        set (stability-⊢ Γ≡Δ ⊢Q) (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ Γ≡Δ ⊢u) (stability-⊢∷ Γ≡Δ ⊢v)
          (stability-⊢∷ Γ≡Δ ⊢w)
      (qrec ⊢C ⊢t ⊢u ⊢v ⊢w) PE.refl →
        let _ , ⊢A , _ , _ , ⊢Q = inversion-Is-set-Cons ⊢v
            ⊢R , R<             = wf-<ˢ (λ ()) ⊢u
            ⊢S , S<             = wf-<ˢ (λ ()) ⊢v
        in
        qrec (stability-⊢ (Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢Q ⟩) ⊢C)
          (stability-⊢∷ (Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A ⟩) ⊢t)
          (stability-⊢∷
             (stability-Resp-Con Γ≡Δ ⊢R ⦃ lt = <ˢ-trans R< ! ⦄) ⊢u)
          (stability-⊢∷
             (stability-Is-set-Con Γ≡Δ ⊢S ⦃ lt = <ˢ-trans S< ! ⦄) ⊢v)
          (stability-⊢∷ Γ≡Δ ⊢w)

  opaque
    unfolding size

    -- Stability for _⊢_∷Level.

    stability-⊢∷L′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      ∇ »⊢ Γ ≡ Δ →
      (⊢l : ∇ » Γ ⊢ l ∷Level) →
      size ⊢l PE.≡ s₂ →
      ∇ » Δ ⊢ l ∷Level
    stability-⊢∷L′ hyp Γ≡Δ = let open Variants hyp in λ where
      (term ok ⊢l) PE.refl →
        term ok (stability-⊢∷ Γ≡Δ ⊢l)
      (literal ok _) _ →
        literal ok (wf-⊢≡ʳ Γ≡Δ)

  opaque
    unfolding Quot-rel-Con Resp-Con size

    -- Stability for _⊢_≡_∷_.

    stability-⊢≡∷′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      ∇ »⊢ Γ ≡ Δ →
      (t≡u : ∇ » Γ ⊢ t ≡ u ∷ A) →
      size t≡u PE.≡ s₂ →
      ∇ » Δ ⊢ t ≡ u ∷ A
    stability-⊢≡∷′ hyp Γ≡Δ = let open Variants hyp in λ where
      (refl ⊢t) PE.refl →
        refl (stability-⊢∷ Γ≡Δ ⊢t)
      (sym ⊢A t₂≡t₁) PE.refl →
        sym (stability-⊢ Γ≡Δ ⊢A) (stability-⊢≡∷ Γ≡Δ t₂≡t₁)
      (trans t₁≡t₂ t₂≡t₃) PE.refl →
        trans (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ t₂≡t₃)
      (conv t₁≡t₂ B≡A) PE.refl →
        conv (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡ Γ≡Δ B≡A)
      (δ-red ⊢Γ α↦t A≡A′ t≡t′) PE.refl →
        δ-red (wf-⊢≡ʳ Γ≡Δ) α↦t A≡A′ t≡t′
      (sucᵘ-cong t₁≡t₂) PE.refl →
        sucᵘ-cong (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
      (supᵘ-cong t₁≡t₂ u₁≡u₂) PE.refl →
        supᵘ-cong (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ u₁≡u₂)
      (supᵘ-zeroˡ l) PE.refl →
        supᵘ-zeroˡ (stability-⊢∷ Γ≡Δ l)
      (supᵘ-sucᵘ l₁ l₂) PE.refl →
        supᵘ-sucᵘ (stability-⊢∷ Γ≡Δ l₁) (stability-⊢∷ Γ≡Δ l₂)
      (supᵘ-assoc l₁ l₂ l₃) PE.refl →
        supᵘ-assoc (stability-⊢∷ Γ≡Δ l₁) (stability-⊢∷ Γ≡Δ l₂) (stability-⊢∷ Γ≡Δ l₃)
      (supᵘ-comm l₁ l₂) PE.refl →
        supᵘ-comm (stability-⊢∷ Γ≡Δ l₁) (stability-⊢∷ Γ≡Δ l₂)
      (supᵘ-idem ⊢l) PE.refl →
        supᵘ-idem (stability-⊢∷ Γ≡Δ ⊢l)
      (supᵘ-sub ⊢l) PE.refl →
        supᵘ-sub (stability-⊢∷ Γ≡Δ ⊢l)
      (U-cong l₁≡l₂) PE.refl →
        U-cong (stability-⊢≡∷ Γ≡Δ l₁≡l₂)
      (Lift-cong ⊢l₁ ⊢l₂ l₂≡l₃ A₁≡A₂) PE.refl →
        Lift-cong (stability-⊢∷L Γ≡Δ ⊢l₁) (stability-⊢∷L Γ≡Δ ⊢l₂)
          (stability-⊢≡∷L Γ≡Δ l₂≡l₃) (stability-⊢≡∷ Γ≡Δ A₁≡A₂)
      (lower-cong x) PE.refl →
        lower-cong (stability-⊢≡∷ Γ≡Δ x)
      (Lift-β x₁ x₂) PE.refl →
        Lift-β (stability-⊢ Γ≡Δ x₁) (stability-⊢∷ Γ≡Δ x₂)
      (Lift-η ⊢l ⊢A ⊢t ⊢u lower-t≡lower-u) PE.refl →
        Lift-η (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢ Γ≡Δ ⊢A)
          (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢∷ Γ≡Δ ⊢u)
          (stability-⊢≡∷ Γ≡Δ lower-t≡lower-u)
      (ΠΣ-cong ⊢l A₁≡A₂ B₁≡B₂ ok) PE.refl →
        let _ , (⊢A₁ , A₁<) = ∙⊢→⊢-<ˢ B₁≡B₂
            ⊢A₁′            = stability-⊢ Γ≡Δ ⊢A₁
                                ⦃ lt = <ˢ-trans A₁< ! ⦄
        in
        ΠΣ-cong (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢≡∷ Γ≡Δ A₁≡A₂)
          (stability-⊢≡∷ (Γ≡Δ ∙⟨ ⊢A₁′ ⟩) B₁≡B₂) ok
      (app-cong t₁≡t₂ u₁≡u₂) PE.refl →
        app-cong (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ u₁≡u₂)
      (β-red ⊢B ⊢t ⊢u eq ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        β-red (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B)
          (stability-⊢∷ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢t) (stability-⊢∷ Γ≡Δ ⊢u) eq ok
      (η-eq ⊢B ⊢t₁ ⊢t₂ t₁0≡t₂0 ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ t₁0≡t₂0
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
            Γ∙A≡Δ∙A       = Γ≡Δ ∙⟨ ⊢A′ ⟩
        in
        η-eq (stability-⊢ Γ∙A≡Δ∙A ⊢B) (stability-⊢∷ Γ≡Δ ⊢t₁)
          (stability-⊢∷ Γ≡Δ ⊢t₂) (stability-⊢≡∷ Γ∙A≡Δ∙A t₁0≡t₂0) ok
      (fst-cong ⊢B t₁≡t₂) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        fst-cong (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
      (snd-cong ⊢B t₁≡t₂) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        snd-cong (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
      (Σ-β₁ ⊢B ⊢t₁ ⊢t₂ eq ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        Σ-β₁ (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) (stability-⊢∷ Γ≡Δ ⊢t₁)
          (stability-⊢∷ Γ≡Δ ⊢t₂) eq ok
      (Σ-β₂ ⊢B ⊢t₁ ⊢t₂ eq ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        Σ-β₂ (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) (stability-⊢∷ Γ≡Δ ⊢t₁)
          (stability-⊢∷ Γ≡Δ ⊢t₂) eq ok
      (Σ-η ⊢B ⊢t₁ ⊢t₂ fst-t₁≡fst-t₂ snd-t₁≡snd-t₂ ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        Σ-η (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B) (stability-⊢∷ Γ≡Δ ⊢t₁)
          (stability-⊢∷ Γ≡Δ ⊢t₂) (stability-⊢≡∷ Γ≡Δ fst-t₁≡fst-t₂)
          (stability-⊢≡∷ Γ≡Δ snd-t₁≡snd-t₂) ok
      (prod-cong ⊢B t₁≡t₂ u₁≡u₂ ok) PE.refl →
        let _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢B
            ⊢A′           = stability-⊢ Γ≡Δ ⊢A ⦃ lt = <ˢ-trans A< ! ⦄
        in
        prod-cong (stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ u₁≡u₂) ok
      (prodrec-cong C₁≡C₂ t₁≡t₂ u₁≡u₂) PE.refl →
        let _ , _ , ok                = inversion-ΠΣ (⊢∙→⊢ (wf C₁≡C₂))
            _ , (⊢A , A<) , (⊢B , B<) = ∙∙⊢→⊢-<ˢ u₁≡u₂
            ⊢A′                       = stability-⊢ Γ≡Δ ⊢A
                                          ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢B′                       = stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B
                                          ⦃ lt = <ˢ-trans B< ! ⦄
        in
        prodrec-cong (stability-⊢≡ (Γ≡Δ ∙⟨ ΠΣⱼ ⊢B′ ok ⟩) C₁≡C₂)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
          (stability-⊢≡∷ (Γ≡Δ ∙⟨ ⊢A′ ⟩ ∙⟨ ⊢B′ ⟩) u₁≡u₂)
      (prodrec-β ⊢C ⊢t ⊢u ⊢v eq) PE.refl →
        let _ , _ , ok                = inversion-ΠΣ (⊢∙→⊢ (wf ⊢C))
            _ , (⊢A , A<) , (⊢B , B<) = ∙∙⊢→⊢-<ˢ ⊢v
            ⊢A′                       = stability-⊢ Γ≡Δ ⊢A
                                          ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢B′                       = stability-⊢ (Γ≡Δ ∙⟨ ⊢A′ ⟩) ⊢B
                                          ⦃ lt = <ˢ-trans B< ! ⦄
        in
        prodrec-β (stability-⊢ (Γ≡Δ ∙⟨ ΠΣⱼ ⊢B′ ok ⟩) ⊢C)
          (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢∷ Γ≡Δ ⊢u)
          (stability-⊢∷ (Γ≡Δ ∙⟨ ⊢A′ ⟩ ∙⟨ ⊢B′ ⟩) ⊢v) eq
      (emptyrec-cong A₁≡A₂ t₁≡t₂) PE.refl →
        emptyrec-cong (stability-⊢≡ Γ≡Δ A₁≡A₂) (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
      (unitrec-cong A₁≡A₂ t₁≡t₂ u₁≡u₂ no-η) PE.refl →
        let ok = inversion-Unit (⊢∙→⊢ (wf A₁≡A₂)) in
        unitrec-cong
          (stability-⊢≡ (Γ≡Δ ∙⟨ univ (Unitⱼ (wf-⊢≡ʳ Γ≡Δ) ok) ⟩) A₁≡A₂)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ u₁≡u₂) no-η
      (unitrec-β ⊢A ⊢t no-η) PE.refl →
        let ok = inversion-Unit (⊢∙→⊢ (wf ⊢A)) in
        unitrec-β
          (stability-⊢ (Γ≡Δ ∙⟨ univ (Unitⱼ (wf-⊢≡ʳ Γ≡Δ) ok) ⟩) ⊢A)
          (stability-⊢∷ Γ≡Δ ⊢t) no-η
      (unitrec-β-η ⊢A ⊢t ⊢u no-η) PE.refl →
        let ok = inversion-Unit (⊢∙→⊢ (wf ⊢A)) in
        unitrec-β-η
          (stability-⊢ (Γ≡Δ ∙⟨ univ (Unitⱼ (wf-⊢≡ʳ Γ≡Δ) ok) ⟩) ⊢A)
          (stability-⊢∷ Γ≡Δ ⊢t) (stability-⊢∷ Γ≡Δ ⊢u) no-η
      (η-unit ⊢t₁ ⊢t₂ η) PE.refl →
        η-unit (stability-⊢∷ Γ≡Δ ⊢t₁) (stability-⊢∷ Γ≡Δ ⊢t₂) η
      (suc-cong t₁≡t₂) PE.refl →
        suc-cong (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
      (natrec-cong A₁≡A₂ t₁≡t₂ u₁≡u₂ v₁≡v₂) PE.refl →
        let ⊢ℕ              = univ (ℕⱼ (wf-⊢≡ʳ Γ≡Δ))
            _ , (⊢A₁ , A₁<) = ∙⊢→⊢-<ˢ u₁≡u₂
            ⊢A₁′            = stability-⊢ (Γ≡Δ ∙⟨ ⊢ℕ ⟩) ⊢A₁
                                ⦃ lt = <ˢ-trans A₁< ! ⦄
        in
        natrec-cong (stability-⊢≡ (Γ≡Δ ∙⟨ ⊢ℕ ⟩) A₁≡A₂)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
          (stability-⊢≡∷ (Γ≡Δ ∙⟨ ⊢ℕ ⟩ ∙⟨ ⊢A₁′ ⟩) u₁≡u₂)
          (stability-⊢≡∷ Γ≡Δ v₁≡v₂)
      (natrec-zero ⊢t ⊢u) PE.refl →
        let ⊢ℕ            = univ (ℕⱼ (wf-⊢≡ʳ Γ≡Δ))
            _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢u
            ⊢A′           = stability-⊢ (Γ≡Δ ∙⟨ ⊢ℕ ⟩) ⊢A
                              ⦃ lt = <ˢ-trans A< ! ⦄
        in
        natrec-zero (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ (Γ≡Δ ∙⟨ ⊢ℕ ⟩ ∙⟨ ⊢A′ ⟩) ⊢u)
      (natrec-suc ⊢t ⊢u ⊢v) PE.refl →
        let ⊢ℕ            = univ (ℕⱼ (wf-⊢≡ʳ Γ≡Δ))
            _ , (⊢A , A<) = ∙⊢→⊢-<ˢ ⊢u
            ⊢A′           = stability-⊢ (Γ≡Δ ∙⟨ ⊢ℕ ⟩) ⊢A
                              ⦃ lt = <ˢ-trans A< ! ⦄
        in
        natrec-suc (stability-⊢∷ Γ≡Δ ⊢t)
          (stability-⊢∷ (Γ≡Δ ∙⟨ ⊢ℕ ⟩ ∙⟨ ⊢A′ ⟩) ⊢u) (stability-⊢∷ Γ≡Δ ⊢v)
      (Id-cong A₁≡A₂ t₁≡t₂ u₁≡u₂) PE.refl →
        Id-cong (stability-⊢≡∷ Γ≡Δ A₁≡A₂) (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
          (stability-⊢≡∷ Γ≡Δ u₁≡u₂)
      (J-cong A₁≡A₂ ⊢t₁ t₁≡t₂ B₁≡B₂ u₁≡u₂ v₁≡v₂ w₁≡w₂) PE.refl →
        let _ , (⊢A₁ , A₁<) , _ = ∙∙⊢→⊢-<ˢ B₁≡B₂
            ⊢A₁′                = stability-⊢ Γ≡Δ ⊢A₁
                                    ⦃ lt = <ˢ-trans A₁< ! ⦄
            ⊢t₁′                = stability-⊢∷ Γ≡Δ ⊢t₁
        in
        J-cong (stability-⊢≡ Γ≡Δ A₁≡A₂) ⊢t₁′
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
          (stability-⊢≡
             (Γ≡Δ
                ∙⟨ ⊢A₁′ ⟩
                ∙⟨ Idⱼ (wk₁ ⊢A₁′ ⊢A₁′) (wk₁ ⊢A₁′ ⊢t₁′)
                     (var₀ ⊢A₁′) ⟩)
             B₁≡B₂)
          (stability-⊢≡∷ Γ≡Δ u₁≡u₂) (stability-⊢≡∷ Γ≡Δ v₁≡v₂)
          (stability-⊢≡∷ Γ≡Δ w₁≡w₂)
      (J-β ⊢t ⊢B ⊢u eq) PE.refl →
        let _ , (⊢A , A<) , _ = ∙∙⊢→⊢-<ˢ ⊢B
            ⊢A′               = stability-⊢ Γ≡Δ ⊢A
                                  ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢t′               = stability-⊢∷ Γ≡Δ ⊢t
        in
        J-β ⊢t′
          (stability-⊢
             (Γ≡Δ
                ∙⟨ ⊢A′ ⟩
                ∙⟨ Idⱼ (wk₁ ⊢A′ ⊢A′) (wk₁ ⊢A′ ⊢t′) (var₀ ⊢A′) ⟩)
             ⊢B)
          (stability-⊢∷ Γ≡Δ ⊢u) eq
      (K-cong A₁≡A₂ t₁≡t₂ B₁≡B₂ u₁≡u₂ v₁≡v₂ ok) PE.refl →
        let _ , ⊢Id                       = ∙⊢→⊢-<ˢ B₁≡B₂
            (⊢A₁ , A₁<) , (⊢t₁ , t₁<) , _ = inversion-Id-⊢-<ˢ ⊢Id
            ⊢A₁′                          = stability-⊢ Γ≡Δ ⊢A₁
                                              ⦃ lt = <ˢ-trans A₁< ! ⦄
            ⊢t₁′                          = stability-⊢∷ Γ≡Δ ⊢t₁
                                              ⦃ lt = <ˢ-trans t₁< ! ⦄
        in
        K-cong (stability-⊢≡ Γ≡Δ A₁≡A₂) (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
          (stability-⊢≡ (Γ≡Δ ∙⟨ Idⱼ ⊢A₁′ ⊢t₁′ ⊢t₁′ ⟩) B₁≡B₂)
          (stability-⊢≡∷ Γ≡Δ u₁≡u₂) (stability-⊢≡∷ Γ≡Δ v₁≡v₂) ok
      (K-β ⊢B ⊢u ok) PE.refl →
        let _ , ⊢Id                   = ∙⊢→⊢-<ˢ ⊢B
            (⊢A , A<) , (⊢t , t<) , _ = inversion-Id-⊢-<ˢ ⊢Id
            ⊢A′                       = stability-⊢ Γ≡Δ ⊢A
                                          ⦃ lt = <ˢ-trans A< ! ⦄
            ⊢t′                       = stability-⊢∷ Γ≡Δ ⊢t
                                          ⦃ lt = <ˢ-trans t< ! ⦄
        in
        K-β (stability-⊢ (Γ≡Δ ∙⟨ Idⱼ ⊢A′ ⊢t′ ⊢t′ ⟩) ⊢B)
          (stability-⊢∷ Γ≡Δ ⊢u) ok
      ([]-cong-cong l₁≡l₂ A₁≡A₂ t₁≡t₂ u₁≡u₂ v₁≡v₂ ok) PE.refl →
        []-cong-cong (stability-⊢≡∷L Γ≡Δ l₁≡l₂)
          (stability-⊢≡ Γ≡Δ A₁≡A₂) (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
          (stability-⊢≡∷ Γ≡Δ u₁≡u₂) (stability-⊢≡∷ Γ≡Δ v₁≡v₂) ok
      ([]-cong-β ⊢l ⊢t eq ok) PE.refl →
        []-cong-β (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢∷ Γ≡Δ ⊢t) eq ok
      (equality-reflection ok ⊢Id ⊢v) PE.refl →
        equality-reflection ok (stability-⊢ Γ≡Δ ⊢Id)
          (stability-⊢∷ Γ≡Δ ⊢v)
      (Quot-cong ok ⊢l A₁≡A₂ B₁≡B₂) PE.refl →
        let _ , ⊢A₁ , ⊢wk1-A₁ = ∙∙⊢→⊢-<ˢ B₁≡B₂
            ΓA₁≡ΔA₁           = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A₁ ⟩
        in
        Quot-cong ok (stability-⊢∷L Γ≡Δ ⊢l) (stability-⊢≡∷ Γ≡Δ A₁≡A₂)
          (stability-⊢≡∷
             (ΓA₁≡ΔA₁ ∙⟨ stability-⊢-<ˢ ΓA₁≡ΔA₁ ⊢wk1-A₁ ⟩) B₁≡B₂)
      (class-cong ⊢Q t₁≡t₂) PE.refl →
        class-cong (stability-⊢ Γ≡Δ ⊢Q) (stability-⊢≡∷ Γ≡Δ t₁≡t₂)
      (resp-cong ok A₁≡A₂ B₁≡B₂ t₁≡t₂ u₁≡u₂ v₁≡v₂) PE.refl →
        let _ , ⊢A₁ , ⊢wk1-A₁ = ∙∙⊢→⊢-<ˢ B₁≡B₂
            ΓA₁≡ΔA₁           = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A₁ ⟩
        in
        resp-cong ok (stability-⊢≡ Γ≡Δ A₁≡A₂)
          (stability-⊢≡ (ΓA₁≡ΔA₁ ∙⟨ stability-⊢-<ˢ ΓA₁≡ΔA₁ ⊢wk1-A₁ ⟩)
             B₁≡B₂)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ u₁≡u₂)
          (stability-⊢≡∷ Γ≡Δ v₁≡v₂)
      (set-cong A₁≡A₂ B₁≡B₂ t₁≡t₂ u₁≡u₂ v₁≡v₂ w₁≡w₂) PE.refl →
        let _ , ⊢A₁ , ⊢wk1-A₁ = ∙∙⊢→⊢-<ˢ B₁≡B₂
            ΓA₁≡ΔA₁           = Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A₁ ⟩
        in
        set-cong (stability-⊢≡ Γ≡Δ A₁≡A₂)
          (stability-⊢≡ (ΓA₁≡ΔA₁ ∙⟨ stability-⊢-<ˢ ΓA₁≡ΔA₁ ⊢wk1-A₁ ⟩)
             B₁≡B₂)
          (stability-⊢≡∷ Γ≡Δ t₁≡t₂) (stability-⊢≡∷ Γ≡Δ u₁≡u₂)
          (stability-⊢≡∷ Γ≡Δ v₁≡v₂) (stability-⊢≡∷ Γ≡Δ w₁≡w₂)
      (qrec-cong C₁≡C₂ t₁≡t₂ u₁≡u₂ v₁≡v₂ w₁≡w₂)
        PE.refl →
        let _ , ⊢A , _ , _ , ⊢Q = inversion-Is-set-Cons v₁≡v₂
            ⊢R , R<             = wf-<ˢ (λ ()) u₁≡u₂
            ⊢S , S<             = wf-<ˢ (λ ()) v₁≡v₂
        in
        qrec-cong (stability-⊢≡ (Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢Q ⟩) C₁≡C₂)
          (stability-⊢≡∷ (Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A ⟩) t₁≡t₂)
          (stability-⊢≡∷
             (stability-Resp-Con Γ≡Δ ⊢R ⦃ lt = <ˢ-trans R< ! ⦄) u₁≡u₂)
          (stability-⊢≡∷
             (stability-Is-set-Con Γ≡Δ ⊢S ⦃ lt = <ˢ-trans S< ! ⦄) v₁≡v₂)
          (stability-⊢≡∷ Γ≡Δ w₁≡w₂)
      (qrec-β ⊢C ⊢t ⊢u ⊢v ⊢w) PE.refl →
        let _ , ⊢A , _ , _ , ⊢Q = inversion-Is-set-Cons ⊢v
            ⊢R , R<             = wf-<ˢ (λ ()) ⊢u
            ⊢S , S<             = wf-<ˢ (λ ()) ⊢v
        in
        qrec-β (stability-⊢ (Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢Q ⟩) ⊢C)
          (stability-⊢∷ (Γ≡Δ ∙⟨ stability-⊢-<ˢ Γ≡Δ ⊢A ⟩) ⊢t)
          (stability-⊢∷
             (stability-Resp-Con Γ≡Δ ⊢R ⦃ lt = <ˢ-trans R< ! ⦄) ⊢u)
          (stability-⊢∷
             (stability-Is-set-Con Γ≡Δ ⊢S ⦃ lt = <ˢ-trans S< ! ⦄) ⊢v)
          (stability-⊢∷ Γ≡Δ ⊢w)

  opaque
    unfolding size

    -- Stability for _⊢_≡_∷Level.

    stability-⊢≡∷L′ :
      (∀ {s₁} → s₁ <ˢ s₂ → P s₁) →
      ∇ »⊢ Γ ≡ Δ →
      (l₁≡l₂ : ∇ » Γ ⊢ l₁ ≡ l₂ ∷Level) →
      size l₁≡l₂ PE.≡ s₂ →
      ∇ » Δ ⊢ l₁ ≡ l₂ ∷Level
    stability-⊢≡∷L′ hyp Γ≡Δ = let open Variants hyp in λ where
      (term ok l₁≡l₂) PE.refl →
        term ok (stability-⊢≡∷ Γ≡Δ l₁≡l₂)
      (literal ok _) _ →
        literal ok (wf-⊢≡ʳ Γ≡Δ)

  opaque

    -- The type P s is inhabited for every s.

    P-inhabited : P s
    P-inhabited =
      well-founded-induction P
        (λ _ hyp →
           record
             { stability-⊢    = stability-⊢′    hyp
             ; stability-⊢≡   = stability-⊢≡′   hyp
             ; stability-⊢∷   = stability-⊢∷′   hyp
             ; stability-⊢∷L  = stability-⊢∷L′  hyp
             ; stability-⊢≡∷  = stability-⊢≡∷′  hyp
             ; stability-⊢≡∷L = stability-⊢≡∷L′ hyp
             })
        _

opaque

  -- Stability for several kinds of judgements.

  stability-⊢ : ∇ »⊢ Γ ≡ Δ → ∇ » Γ ⊢[ 𝓙 ] → ∇ » Δ ⊢[ 𝓙 ]
  stability-⊢ {𝓙 = [ctxt]} Γ≡Δ _ =
    wf-⊢≡ʳ Γ≡Δ
  stability-⊢ {𝓙 = [ _ type]} Γ≡Δ ⊢𝓙 =
    P.stability-⊢ Inhabited.P-inhabited Γ≡Δ ⊢𝓙 PE.refl
  stability-⊢ {𝓙 = [ _ ≡ _ type]} Γ≡Δ ⊢𝓙 =
    P.stability-⊢≡ Inhabited.P-inhabited Γ≡Δ ⊢𝓙 PE.refl
  stability-⊢ {𝓙 = [ _ ∷ _ ]} Γ≡Δ ⊢𝓙 =
    P.stability-⊢∷ Inhabited.P-inhabited Γ≡Δ ⊢𝓙 PE.refl
  stability-⊢ {𝓙 = [ _ ≡ _ ∷ _ ]} Γ≡Δ ⊢𝓙 =
    P.stability-⊢≡∷ Inhabited.P-inhabited Γ≡Δ ⊢𝓙 PE.refl
  stability-⊢ {𝓙 = [ _ ∷Level]} Γ≡Δ ⊢𝓙 =
    P.stability-⊢∷L Inhabited.P-inhabited Γ≡Δ ⊢𝓙 PE.refl
  stability-⊢ {𝓙 = [ _ ≡ _ ∷Level]} Γ≡Δ ⊢𝓙 =
    P.stability-⊢≡∷L Inhabited.P-inhabited Γ≡Δ ⊢𝓙 PE.refl

opaque

  -- A stability lemma related to Resp-Con.

  stability-Resp-Con :
    ∇ »⊢ Γ ≡ Δ →
    ∇ »⊢ Resp-Con Γ A B →
    ∇ »⊢ Resp-Con Γ A B ≡ Resp-Con Δ A B
  stability-Resp-Con Γ≡Δ ⊢R =
    Variants.stability-Resp-Con (λ _ → Inhabited.P-inhabited) Γ≡Δ ⊢R
      ⦃ lt = ∃-<ˢ .proj₂ ⦄

opaque

  -- A stability lemma related to Is-set-Con.

  stability-Is-set-Con :
    ∇ »⊢ Γ ≡ Δ →
    ∇ »⊢ Is-set-Con Γ A B C →
    ∇ »⊢ Is-set-Con Γ A B C ≡ Is-set-Con Δ A B C
  stability-Is-set-Con Γ≡Δ ⊢S =
    Variants.stability-Is-set-Con (λ _ → Inhabited.P-inhabited) Γ≡Δ ⊢S
      ⦃ lt = ∃-<ˢ .proj₂ ⦄