------------------------------------------------------------------------
-- The algorithmic equality is decidable (in the absence of equality
-- reflection)
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality
import Tools.PropositionalEquality as PE
open import Tools.Relation

module Definition.Conversion.Decidable
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  (open Type-restrictions R)
  (_≟_ : Decidable (PE._≡_ {A = M}))
  ⦃ no-equality-reflection : No-equality-reflection ⦄
  where

open import Definition.Untyped M
import Definition.Untyped.Erased 𝕄 as Erased
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Properties M
open import Definition.Untyped.Properties.Neutral M type-variant
open import Definition.Typed R
open import Definition.Typed.EqRelInstance R
open import Definition.Typed.EqualityRelation.Instance R
open import Definition.Typed.Inversion R
open import Definition.Typed.Properties R
open import Definition.Typed.Reasoning.Type R
open import Definition.Typed.Stability R
open import Definition.Typed.Substitution R
open import Definition.Typed.Syntactic R
open import Definition.Conversion R
open import Definition.Conversion.Inversion R
open import Definition.Conversion.Whnf R
open import Definition.Conversion.Soundness R
open import Definition.Conversion.Symmetry R
open import Definition.Conversion.Stability R
open import Definition.Conversion.Conversion R
open import Definition.Typed.Consequences.Injectivity R
open import Definition.Typed.Consequences.Reduction R
open import Definition.Typed.Consequences.Equality R
open import Definition.Typed.Consequences.NeTypeEq R

open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Product
open import Tools.Empty
open import Tools.Sum using (inj₁; inj₂)

private
  variable
    ℓ : Nat
    Γ Δ : Con Term ℓ
    A A₁ A₂ A′ B B₁ B₂ B′ C₁ C₂ t t₁ t₂ t′ u u₁ u₂ v₁ v₂ w₁ w₂ : Term _
    b₁ b₂ : BinderMode
    s₁ s₂ : Strength
    l l₁ l₂ : Universe-level
    p p₁ p₂ p′ q q₁ q₂ q′ q′₁ q′₂ r₁ r₂ : M

------------------------------------------------------------------------
-- Private definitions

private opaque

  -- Some lemmas used below.

  ~↓→∷ : Γ ⊢ t ~ u ↓ A → Γ ⊢ t ∷ A
  ~↓→∷ = proj₁ ∘→ proj₂ ∘→ syntacticEqTerm ∘→ soundness~↓

  [conv↓]∷→∷ : Γ ⊢ t [conv↓] u ∷ A → Γ ⊢ t ∷ A
  [conv↓]∷→∷ = proj₁ ∘→ proj₂ ∘→ syntacticEqTerm ∘→ soundnessConv↓Term

  ~↓→∷→Whnf×≡ : Γ ⊢ t ~ u ↓ A → Γ ⊢ t ∷ B → Γ ⊢ B ≡ A × Whnf A
  ~↓→∷→Whnf×≡ t~u ⊢t =
    let A-whnf , t-ne , _ = ne~↓ t~u in
    neTypeEq t-ne ⊢t (~↓→∷ t~u) , A-whnf

private opaque

  -- A lemma used below.

  [conv↓]∷ℕ→~↓ℕ :
    Γ ⊢ t ~ t′ ↓ ℕ →
    Γ ⊢ t [conv↓] u ∷ ℕ →
    Γ ⊢ t ~ u ↓ ℕ
  [conv↓]∷ℕ→~↓ℕ ([~] _ _ t~t′) t≡u =
    case inv-[conv↓]∷-ℕ t≡u of λ where
      (inj₁ t~u)                          → t~u
      (inj₂ (inj₁ (PE.refl , _)))         → ⊥-elim (inv-zero~ t~t′)
      (inj₂ (inj₂ (_ , _ , PE.refl , _))) → ⊥-elim (inv-suc~ t~t′)

private opaque

  -- A lemma used below.

  [conv↓]∷Σʷ→~↓ :
    Γ ⊢ t ~ t′ ↓ Σʷ p′ , q′ ▷ A′ ▹ B′ →
    Γ ⊢ t [conv↓] u ∷ Σʷ p , q ▷ A ▹ B →
    ∃ λ C → Γ ⊢ t ~ u ↓ C
  [conv↓]∷Σʷ→~↓ ([~] _ _ t~t′) t≡u =
    case inv-[conv↓]∷-Σʷ t≡u of λ where
      (inj₁ (_ , _ , _ , _ , t~u))         → _ , t~u
      (inj₂ (_ , _ , _ , _ , PE.refl , _)) → ⊥-elim (inv-prod~ t~t′)

private opaque

  -- A lemma used below.

  ≡starʷ→~↓Unitʷ→Unitʷ-η :
    Γ ⊢ t ~ u ↓ Unitʷ l →
    Γ ⊢ t [conv↓] starʷ l ∷ Unitʷ l →
    Unitʷ-η
  ≡starʷ→~↓Unitʷ→Unitʷ-η ([~] _ _ t~u) t≡star =
    case inv-[conv↓]∷-Unitʷ t≡star of λ where
      (inj₂ (η , _))                       → η
      (inj₁ (no-η , inj₁ ([~] _ _ ~star))) → ⊥-elim (inv-~star ~star)
      (inj₁ (no-η , inj₂ (PE.refl , _)))   → ⊥-elim (inv-star~ t~u)

private opaque

  -- A lemma used below.

  dec~↑-app-cong :
    Γ ⊢ t₁ ∷ Π p₁ , q₁ ▷ A₁ ▹ B₁ →
    Γ ⊢ u₁ ∷ Π p₂ , q₂ ▷ A₂ ▹ B₂ →
    Dec (∃ λ C → Γ ⊢ t₁ ~ u₁ ↓ C) →
    (Γ ⊢ A₁ ≡ A₂ → Dec (Γ ⊢ t₂ [conv↑] u₂ ∷ A₁)) →
    Dec (∃ λ C → Γ ⊢ t₁ ∘⟨ p₁ ⟩ t₂ ~ u₁ ∘⟨ p₂ ⟩ u₂ ↑ C)
  dec~↑-app-cong
    {p₁} {q₁} {A₁} {B₁} {p₂} {q₂} {A₂} {B₂}
    ⊢t₁ ⊢u₁ (yes (C , t₁~u₁)) dec₂ =
    let C-whnf , t₁-ne , u₁-ne = ne~↓ t₁~u₁
        _ , ⊢t₁′ , ⊢u₁′        = syntacticEqTerm (soundness~↓ t₁~u₁)
        Π≡C                    = neTypeEq t₁-ne ⊢t₁ ⊢t₁′
        A₁≡A₂ , _ , p₁≡p₂ , _  =
          ΠΣ-injectivity
            (Π p₁ , q₁ ▷ A₁ ▹ B₁  ≡⟨ Π≡C ⟩⊢
             C                    ≡˘⟨ neTypeEq u₁-ne ⊢u₁ ⊢u₁′ ⟩⊢∎
             Π p₂ , q₂ ▷ A₂ ▹ B₂  ∎)
    in
    case dec₂ A₁≡A₂ of λ where
      (yes t₂≡u₂) →
        yes $
        let _ , _ , C≡Π = ΠΣ≡Whnf Π≡C C-whnf in
          _
        , PE.subst (flip (_⊢_~_↑_ _ _) _)
            (PE.cong (_ ∘⟨_⟩ _) p₁≡p₂)
            (app-cong (PE.subst (_⊢_~_↓_ _ _ _) C≡Π t₁~u₁)
               (convConv↑Term
                  (ΠΣ-injectivity (PE.subst (_⊢_≡_ _ _) C≡Π Π≡C) .proj₁)
                  t₂≡u₂))
      (no t₂≢u₂) →
        no λ (_ , t~u) →
        let _ , _ , _ , _ , _ , _ , u≡∘ , t₁~ , t₂≡ = inv-∘~ t~u
            _ , _ , ≡u₂                             =
              ∘-PE-injectivity (PE.sym u≡∘)
            Π≡Π = neTypeEq t₁-ne ⊢t₁ (~↓→∷ t₁~)
        in
        t₂≢u₂ $
        convConv↑Term (sym (ΠΣ-injectivity Π≡Π .proj₁)) $
        PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ t₂≡
  dec~↑-app-cong _ _ (no ¬t₁~u₁) _ =
    no λ (_ , t~u) →
    let _ , _ , _ , _ , _ , _ , u≡∘ , t₁~ , _ = inv-∘~ t~u
        _ , ≡u₁ , _                           =
          ∘-PE-injectivity (PE.sym u≡∘)
    in
    ¬t₁~u₁ (_ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡u₁ t₁~)

private opaque

  -- A lemma used below.

  dec~↑-fst-cong :
    Γ ⊢ t ∷ Σˢ p , q ▷ A ▹ B →
    Dec (p PE.≡ p′ × ∃ λ C → Γ ⊢ t ~ u ↓ C) →
    Dec (∃ λ C → Γ ⊢ fst p t ~ fst p′ u ↑ C)
  dec~↑-fst-cong ⊢t (yes (PE.refl , _ , t~u)) =
    yes $
    let _ , _ , C≡Σ = uncurry ΠΣ≡Whnf (~↓→∷→Whnf×≡ t~u ⊢t) in
    _ , fst-cong (PE.subst (_⊢_~_↓_ _ _ _) C≡Σ t~u)
  dec~↑-fst-cong _ (no not-both-equal) =
    no λ (_ , fst-t~fst-u) →
    case inv-fst~ fst-t~fst-u of λ {
      (_ , _ , _ , PE.refl , t~) →
    not-both-equal (PE.refl , _ , t~) }

private opaque

  -- A lemma used below.

  dec~↑-snd-cong :
    Γ ⊢ t ∷ Σˢ p , q ▷ A ▹ B →
    Dec (p PE.≡ p′ × ∃ λ C → Γ ⊢ t ~ u ↓ C) →
    Dec (∃ λ C → Γ ⊢ snd p t ~ snd p′ u ↑ C)
  dec~↑-snd-cong ⊢t (yes (PE.refl , _ , t~u)) =
    yes $
    let _ , _ , C≡Σ = uncurry ΠΣ≡Whnf (~↓→∷→Whnf×≡ t~u ⊢t) in
    _ , snd-cong (PE.subst (_⊢_~_↓_ _ _ _) C≡Σ t~u)
  dec~↑-snd-cong _ (no not-both-equal) =
    no λ (_ , snd-t~snd-u) →
    case inv-snd~ snd-t~snd-u of λ {
      (_ , _ , _ , _ , _ , PE.refl , t~) →
    not-both-equal (PE.refl , _ , t~) }

private opaque

  -- A lemma used below.

  dec~↑-prodrec-cong :
    Γ ⊢ t₁ ∷ Σʷ p₁ , q₁ ▷ A₁ ▹ B₁ →
    Γ ⊢ t₂ ∷ Σʷ p₂ , q₂ ▷ A₂ ▹ B₂ →
    Dec
      (r₁ PE.≡ r₂ × q′₁ PE.≡ q′₂ ×
       ∃ λ D → Γ ⊢ t₁ ~ t₂ ↓ D) →
    (⊢ Γ ∙ Σʷ p₁ , q₁ ▷ A₁ ▹ B₁ ≡ Γ ∙ Σʷ p₂ , q₂ ▷ A₂ ▹ B₂ →
     Dec (Γ ∙ Σʷ p₁ , q₁ ▷ A₁ ▹ B₁ ⊢ C₁ [conv↑] C₂)) →
    (⊢ Γ ∙ A₂ ∙ B₂ ≡ Γ ∙ A₁ ∙ B₁ →
     Γ ∙ A₂ ∙ B₂ ⊢ C₂ [ prodʷ p₂ (var x1) (var x0) ]↑² ≡
       C₁ [ prodʷ p₁ (var x1) (var x0) ]↑² →
     Dec
       (Γ ∙ A₁ ∙ B₁ ⊢ u₁ [conv↑] u₂ ∷
          C₁ [ prodʷ p₁ (var x1) (var x0) ]↑²)) →
    Dec
      (∃ λ D →
       Γ ⊢ prodrec r₁ p₁ q′₁ C₁ t₁ u₁ ~ prodrec r₂ p₂ q′₂ C₂ t₂ u₂ ↑ D)
  dec~↑-prodrec-cong
    {p₁} {q₁} {A₁} {B₁} {p₂} {q₂} {A₂} {B₂}
    ⊢t₁ ⊢t₂ (yes (PE.refl , PE.refl , D , t₁~t₂)) dec₁ dec₃ =
    let D-whnf , t₁-ne , t₂-ne = ne~↓ t₁~t₂
        _ , ⊢t₁′ , ⊢t₂′        = syntacticEqTerm (soundness~↓ t₁~t₂)
        Σ₁≡D                   = neTypeEq t₁-ne ⊢t₁ ⊢t₁′
        Σ₁≡Σ₂                  =
          Σʷ p₁ , q₁ ▷ A₁ ▹ B₁  ≡⟨ Σ₁≡D ⟩⊢
          D                     ≡⟨ neTypeEq t₂-ne ⊢t₂′ ⊢t₂ ⟩⊢∎
          Σʷ p₂ , q₂ ▷ A₂ ▹ B₂  ∎
        A₁≡A₂ , B₁≡B₂ , p₁≡p₂ , _ =
          ΠΣ-injectivity-no-equality-reflection Σ₁≡Σ₂
        ΓA₁B₁≡ΓA₂B₂ = refl-∙ A₁≡A₂ ⊢_≡_.∙ B₁≡B₂
    in
    case p₁≡p₂ of λ {
      PE.refl →
    case (dec₁ (refl-∙ Σ₁≡Σ₂)
            ×-dec′ λ C₁≡C₂ →
          dec₃
            (symConEq ΓA₁B₁≡ΓA₂B₂)
             (_⊢_≡_.sym $
              stabilityEq ΓA₁B₁≡ΓA₂B₂ $
              subst↑²TypeEq-prod (soundnessConv↑ C₁≡C₂))) of λ where
      (yes (C₁≡C₂ , u₁≡u₂)) →
        yes $
        case ΠΣ≡Whnf Σ₁≡D D-whnf of λ {
          (_ , _ , PE.refl) →
        let A₁≡ , B₁≡ , _ =
              ΠΣ-injectivity-no-equality-reflection Σ₁≡D
        in
          _
        , prodrec-cong (stabilityConv↑ (refl-∙ Σ₁≡D) C₁≡C₂) t₁~t₂
            (stabilityConv↑Term (refl-∙ A₁≡ ∙ B₁≡) u₁≡u₂) }
      (no not-both-equal) →
        no λ (_ , pr~pr) →
        let _ , _ , _ , _ , _ , _ , _ , pr≡pr , C₁≡ , t₁~ , u₁≡ =
              inv-prodrec~ pr~pr
            ≡A₁ , ≡B₁ , _ =
              ΠΣ-injectivity-no-equality-reflection
                (neTypeEq t₁-ne (~↓→∷ t₁~) ⊢t₁)
            _ , _ , _ , ≡C₂ , _ , ≡u₂ =
              prodrec-PE-injectivity (PE.sym pr≡pr)
        in
        not-both-equal
          ( stabilityConv↑ (refl-∙ (neTypeEq t₁-ne (~↓→∷ t₁~) ⊢t₁))
              (PE.subst (_⊢_[conv↑]_ _ _) ≡C₂ C₁≡)
          , stabilityConv↑Term (refl-∙ ≡A₁ ∙ ≡B₁)
              (PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡)
          ) }
  dec~↑-prodrec-cong _ _ (no not-all-equal) _ _ =
    no λ (_ , pr~pr) →
    let _ , _ , _ , _ , _ , _ , _ , pr≡pr , _ , t₁~ , _ =
          inv-prodrec~ pr~pr
        r₁≡r₂ , _ , q′₁≡q′₂ , _ , ≡t₂ , _ =
          prodrec-PE-injectivity (PE.sym pr≡pr)
    in
    not-all-equal
      ( r₁≡r₂
      , q′₁≡q′₂
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡t₂ t₁~
      )

private opaque

  -- A lemma used below.

  dec~↑-emptyrec-cong :
    Γ ⊢ t₁ ∷ Empty →
    Dec
      (p₁ PE.≡ p₂ ×
       Γ ⊢ A₁ [conv↑] A₂ ×
       ∃ λ B → Γ ⊢ t₁ ~ t₂ ↓ B) →
    Dec (∃ λ B → Γ ⊢ emptyrec p₁ A₁ t₁ ~ emptyrec p₂ A₂ t₂ ↑ B)
  dec~↑-emptyrec-cong ⊢t₁ (yes (PE.refl , A₁≡A₂ , _ , t₁~t₂)) =
    yes $
    case uncurry Empty≡A (~↓→∷→Whnf×≡ t₁~t₂ ⊢t₁) of λ {
      PE.refl →
    _ , emptyrec-cong A₁≡A₂ t₁~t₂ }
  dec~↑-emptyrec-cong _ (no not-all-equal) =
    no λ (_ , er~er) →
    let _ , _ , _ , er≡er , A₁≡ , t₁~ = inv-emptyrec~ er~er
        p₁≡p₂ , ≡A₂ , ≡t₂             =
          emptyrec-PE-injectivity (PE.sym er≡er)
    in
    not-all-equal
      ( p₁≡p₂
      , PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡t₂ t₁~
      )

private opaque

  -- A lemma used below.

  dec~↑-unitrec-cong :
    ¬ Unitʷ-η →
    Γ ⊢ t₁ ∷ Unitʷ l₁ →
    Dec
      (l₁ PE.≡ l₂ × p₁ PE.≡ p₂ × q₁ PE.≡ q₂ ×
       ∃ λ B → Γ ⊢ t₁ ~ t₂ ↓ B) →
    (⊢ Γ ∙ Unitʷ l₁ ≡ Γ ∙ Unitʷ l₂ →
     Dec (Γ ∙ Unitʷ l₁ ⊢ A₁ [conv↑] A₂)) →
    (Γ ⊢ A₁ [ starʷ l₁ ]₀ ≡ A₂ [ starʷ l₂ ]₀ →
     Dec (Γ ⊢ u₁ [conv↑] u₂ ∷ A₁ [ starʷ l₁ ]₀)) →
    Dec
      (∃ λ B →
       Γ ⊢ unitrec l₁ p₁ q₁ A₁ t₁ u₁ ~ unitrec l₂ p₂ q₂ A₂ t₂ u₂ ↑ B)
  dec~↑-unitrec-cong
    no-η ⊢t₁ (yes (PE.refl , PE.refl , PE.refl , _ , t₁~t₂)) dec₁ dec₂ =
    case
      (dec₁ (reflConEq (∙ syntacticTerm ⊢t₁)) ×-dec′ λ A₁≡A₂ →
       dec₂
         (substTypeEq (soundnessConv↑ A₁≡A₂) $
          _⊢_≡_∷_.refl $
          starⱼ (wfTerm ⊢t₁) (⊢∷Unit→Unit-allowed ⊢t₁)))
      of λ where
      (yes (A₁≡A₂ , u₁≡u₂)) →
        yes $
        let B≡Unit = uncurry Unit≡A (~↓→∷→Whnf×≡ t₁~t₂ ⊢t₁) in
          _
        , unitrec-cong A₁≡A₂ (PE.subst (_⊢_~_↓_ _ _ _) B≡Unit t₁~t₂)
            u₁≡u₂ no-η
      (no not-both-equal) →
        no λ (_ , ur~ur) →
        let _ , _ , _ , _ , ur≡ur , A₁≡ , _ , u₁≡ , _ =
              inv-unitrec~ ur~ur
            _ , _ , _ , ≡A₂ , _ , ≡u₂ =
              unitrec-PE-injectivity (PE.sym ur≡ur)
        in
        not-both-equal
          ( PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡
          )
  dec~↑-unitrec-cong _ _ (no not-all-equal) _ _ =
    no λ (_ , ur~ur) →
    let _ , _ , _ , _ , ur≡ur , _ , t₁~ , _ = inv-unitrec~ ur~ur
        l₁≡l₂ , p₁≡p₂ , q₁≡q₂ , _ , ≡t₂ , _ =
          unitrec-PE-injectivity (PE.sym ur≡ur)
    in
    not-all-equal
      ( l₁≡l₂
      , p₁≡p₂
      , q₁≡q₂
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡t₂ t₁~
      )

private opaque

  -- A lemma used below.

  dec~↑-natrec-cong :
    Γ ⊢ v₁ ∷ ℕ →
    Dec
      (p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × r₁ PE.≡ r₂ ×
       Γ ∙ ℕ ⊢ A₁ [conv↑] A₂ ×
       ∃ λ B → Γ ⊢ v₁ ~ v₂ ↓ B) →
    (Γ ⊢ A₁ [ zero ]₀ ≡ A₂ [ zero ]₀ →
     Dec (Γ ⊢ t₁ [conv↑] t₂ ∷ A₁ [ zero ]₀)) →
    (⊢ Γ ∙ ℕ ∙ A₂ ≡ Γ ∙ ℕ ∙ A₁ →
     Γ ∙ ℕ ∙ A₂ ⊢ A₂ [ suc (var x1) ]↑² ≡ A₁ [ suc (var x1) ]↑² →
     Dec (Γ ∙ ℕ ∙ A₁ ⊢ u₁ [conv↑] u₂ ∷ A₁ [ suc (var x1) ]↑²)) →
    Dec
      (∃ λ B →
       Γ ⊢ natrec p₁ q₁ r₁ A₁ t₁ u₁ v₁ ~
         natrec p₂ q₂ r₂ A₂ t₂ u₂ v₂ ↑ B)
  dec~↑-natrec-cong
    ⊢v₁ (yes (PE.refl , PE.refl , PE.refl , A₁≡A₂ , _ , v₁~v₂)) dec₁
    dec₂ =
    case
      (let A₁≡A₂     = soundnessConv↑ A₁≡A₂
           ⊢Γ        = wfTerm ⊢v₁
           ΓℕA₁≡ΓℕA₂ = refl-∙ (sym A₁≡A₂)
       in
       dec₁ (substTypeEq A₁≡A₂ (refl (zeroⱼ ⊢Γ)))
         ×-dec
       dec₂ ΓℕA₁≡ΓℕA₂
         (stabilityEq (symConEq ΓℕA₁≡ΓℕA₂) $ sym $ sucCong A₁≡A₂))
      of λ where
      (yes (t₁≡t₂ , u₁≡u₂)) →
        yes $
        let B≡ℕ = uncurry ℕ≡A (~↓→∷→Whnf×≡ v₁~v₂ ⊢v₁) in
          _
        , natrec-cong A₁≡A₂ t₁≡t₂ u₁≡u₂
            (PE.subst (_⊢_~_↓_ _ _ _) B≡ℕ v₁~v₂)
      (no not-both-equal) →
        no λ (_ , nr~nr) →
        let _ , _ , _ , _ , _ , nr≡nr , _ , t₁≡ , u₁≡ , _ =
              inv-natrec~ nr~nr
            _ , _ , _ , _ , ≡t₂ , ≡u₂ , _ =
              natrec-PE-injectivity (PE.sym nr≡nr)
        in
        not-both-equal
          ( PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡t₂ t₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡
          )
  dec~↑-natrec-cong _ (no not-all-equal) _ _ =
    no λ (_ , nr~nr) →
    let _ , _ , _ , _ , _ , nr≡nr , A₁≡ , _ , _ , v₁~ =
          inv-natrec~ nr~nr
        p₁≡p₂ , q₁≡q₂ , r₁≡r₂ , ≡A₂ , _ , _ , ≡v₂ =
          natrec-PE-injectivity (PE.sym nr≡nr)
    in
    not-all-equal
      ( p₁≡p₂
      , q₁≡q₂
      , r₁≡r₂
      , PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡v₂ v₁~
      )

private opaque

  -- A lemma used below.

  dec~↑-J-cong :
    Γ ⊢ w₁ ∷ Id A₁ t₁ v₁ →
    Dec
      (p₁ PE.≡ p₂ × q₁ PE.≡ q₂ ×
       Γ ⊢ A₁ [conv↑] A₂ ×
       ∃ λ C → Γ ⊢ w₁ ~ w₂ ↓ C) →
    (Γ ⊢ A₁ ≡ A₂ → Dec (Γ ⊢ t₁ [conv↑] t₂ ∷ A₁)) →
    (⊢ Γ ∙ A₁ ∙ Id (wk1 A₁) (wk1 t₁) (var x0) ≡
       Γ ∙ A₂ ∙ Id (wk1 A₂) (wk1 t₂) (var x0) →
     Dec (Γ ∙ A₁ ∙ Id (wk1 A₁) (wk1 t₁) (var x0) ⊢ B₁ [conv↑] B₂)) →
    (Γ ⊢ B₁ [ t₁ , rfl ]₁₀ ≡ B₂ [ t₂ , rfl ]₁₀ →
     Dec (Γ ⊢ u₁ [conv↑] u₂ ∷ B₁ [ t₁ , rfl ]₁₀)) →
    (Γ ⊢ A₁ ≡ A₂ → Dec (Γ ⊢ v₁ [conv↑] v₂ ∷ A₁)) →
    Dec
      (∃ λ C →
       Γ ⊢ J p₁ q₁ A₁ t₁ B₁ u₁ v₁ w₁ ~ J p₂ q₂ A₂ t₂ B₂ u₂ v₂ w₂ ↑ C)
  dec~↑-J-cong _ (no not-all-equal) _ _ _ _ =
    no λ (_ , J~J) →
    let _ , _ , _ , _ , _ , _ , _ , _ , J≡J , A₁≡ , _ , _ , _ , _ ,
          w₁~ , _ = inv-J~ J~J
        p₁≡p₂ , q₁≡q₂ , ≡A₂ , _ , _ , _ , _ , ≡w₂ =
          J-PE-injectivity (PE.sym J≡J)
    in
    not-all-equal
      ( p₁≡p₂
      , q₁≡q₂
      , PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡w₂ w₁~
      )
  dec~↑-J-cong
    ⊢w₁ (yes (PE.refl , PE.refl , A₁≡A₂ , _ , w₁~w₂))
    dec₁ dec₂ dec₃ dec₄ =
    case
      (let A₁≡A₂ = soundnessConv↑ A₁≡A₂ in
       dec₁ A₁≡A₂
         ×-dec′ λ t₁≡t₂ →
       let t₁≡t₂ = soundnessConv↑Term t₁≡t₂ in
       dec₂ (J-motive-context-cong′ A₁≡A₂ t₁≡t₂)
         ×-dec′ λ B₁≡B₂ →
       dec₃ (J-motive-rfl-cong (soundnessConv↑ B₁≡B₂) t₁≡t₂)
         ×-dec
       dec₄ A₁≡A₂)
      of λ where
      (yes (t₁≡t₂ , B₁≡B₂ , u₁≡u₂ , v₁≡v₂)) →
        yes $
          _
        , J-cong A₁≡A₂ t₁≡t₂ B₁≡B₂ u₁≡u₂ v₁≡v₂ w₁~w₂
            (neTypeEq (ne~↓ w₁~w₂ .proj₂ .proj₁) (~↓→∷ w₁~w₂) ⊢w₁)
      (no not-all-equal) →
        no λ (_ , J~J) →
        let _ , _ , _ , _ , _ , _ , _ , _ , J≡J , _ , t₁≡ , B₁≡ , u₁≡ ,
              v₁≡ , _ = inv-J~ J~J
            _ , _ , _ , ≡t₂ , ≡B₂ , ≡u₂ , ≡v₂ , _ =
              J-PE-injectivity (PE.sym J≡J)
        in
        not-all-equal
          ( PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡t₂ t₁≡
          , PE.subst (_⊢_[conv↑]_ _ _) ≡B₂ B₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡v₂ v₁≡
          )

private opaque

  -- A lemma used below.

  dec~↑-K-cong :
    K-allowed →
    Γ ⊢ v₁ ∷ Id A₁ t₁ t₁ →
    Dec
      (p₁ PE.≡ p₂ ×
       Γ ⊢ A₁ [conv↑] A₂ ×
       ∃ λ C → Γ ⊢ v₁ ~ v₂ ↓ C) →
    (Γ ⊢ A₁ ≡ A₂ → Dec (Γ ⊢ t₁ [conv↑] t₂ ∷ A₁)) →
    (⊢ Γ ∙ Id A₁ t₁ t₁ ≡ Γ ∙ Id A₂ t₂ t₂ →
     Dec (Γ ∙ Id A₁ t₁ t₁ ⊢ B₁ [conv↑] B₂)) →
    (Γ ⊢ B₁ [ rfl ]₀ ≡ B₂ [ rfl ]₀ →
     Dec (Γ ⊢ u₁ [conv↑] u₂ ∷ B₁ [ rfl ]₀)) →
    Dec (∃ λ C → Γ ⊢ K p₁ A₁ t₁ B₁ u₁ v₁ ~ K p₂ A₂ t₂ B₂ u₂ v₂ ↑ C)
  dec~↑-K-cong _ _ (no not-all-equal) _ _ _ =
    no λ (_ , K~K) →
    let _ , _ , _ , _ , _ , _ , _ , K≡K , A₁≡ , _ , _ , _ , v₁~ , _ =
          inv-K~ K~K
        p₁≡p₂ , ≡A₂ , _ , _ , _ , ≡v₂ = K-PE-injectivity (PE.sym K≡K)
    in
    not-all-equal
      ( p₁≡p₂
      , PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡v₂ v₁~
      )
  dec~↑-K-cong
    ok ⊢v₁ (yes (PE.refl , A₁≡A₂ , _ , v₁~v₂)) dec₁ dec₂ dec₃ =
    case
      (let A₁≡A₂ = soundnessConv↑ A₁≡A₂ in
       dec₁ A₁≡A₂
         ×-dec′ λ t₁≡t₂ →
       let t₁≡t₂ = soundnessConv↑Term t₁≡t₂ in
       dec₂ (K-motive-context-cong′ A₁≡A₂ t₁≡t₂)
         ×-dec′ λ B₁≡B₂ →
       dec₃ (K-motive-rfl-cong (soundnessConv↑ B₁≡B₂)))
      of λ where
      (yes (t₁≡t₂ , B₁≡B₂ , u₁≡u₂)) →
        yes $
          _
        , K-cong A₁≡A₂ t₁≡t₂ B₁≡B₂ u₁≡u₂ v₁~v₂
            (neTypeEq (ne~↓ v₁~v₂ .proj₂ .proj₁) (~↓→∷ v₁~v₂) ⊢v₁) ok
      (no not-all-equal) →
        no λ (_ , K~K) →
        let _ , _ , _ , _ , _ , _ , _ , K≡K , _ , t₁≡ , B₁≡ , u₁≡ , _ =
              inv-K~ K~K
            _ , _ , ≡t₂ , ≡B₂ , ≡u₂ , _ = K-PE-injectivity (PE.sym K≡K)
        in
        not-all-equal
          ( PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡t₂ t₁≡
          , PE.subst (_⊢_[conv↑]_ _ _) ≡B₂ B₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡
          )

private opaque

  -- A lemma used below.

  dec~↑-[]-cong-cong :
    let open Erased s₁ in
    []-cong-allowed s₁ →
    Γ ⊢ v₁ ∷ Id A₁ t₁ u₁ →
    Dec
      (s₁ PE.≡ s₂ ×
       Γ ⊢ A₁ [conv↑] A₂ ×
       ∃ λ B → Γ ⊢ v₁ ~ v₂ ↓ B) →
    (Γ ⊢ A₁ ≡ A₂ → Dec (Γ ⊢ t₁ [conv↑] t₂ ∷ A₁)) →
    (Γ ⊢ A₁ ≡ A₂ → Dec (Γ ⊢ u₁ [conv↑] u₂ ∷ A₁)) →
    Dec
      (∃ λ B → Γ ⊢ []-cong s₁ A₁ t₁ u₁ v₁ ~ []-cong s₂ A₂ t₂ u₂ v₂ ↑ B)
  dec~↑-[]-cong-cong
    ok ⊢v₁ (yes (PE.refl , A₁≡A₂ , _ , v₁~v₂)) dec₁ dec₂ =
    case
       (let A₁≡A₂ = soundnessConv↑ A₁≡A₂ in
        dec₁ A₁≡A₂ ×-dec dec₂ A₁≡A₂)
      of λ where
      (yes (t₁≡t₂ , u₁≡u₂)) →
        yes $
          _
        , []-cong-cong A₁≡A₂ t₁≡t₂ u₁≡u₂ v₁~v₂
            (neTypeEq (ne~↓ v₁~v₂ .proj₂ .proj₁) (~↓→∷ v₁~v₂) ⊢v₁) ok
      (no not-both-equal) →
        no λ (_ , bc~bc) →
        let _ , _ , _ , _ , _ , _ , bc≡bc , _ , t₁≡ , u₁≡ , _ =
              inv-[]-cong~ bc~bc
            _ , _ , ≡t₂ , ≡u₂ , _ =
              []-cong-PE-injectivity (PE.sym bc≡bc)
        in
        not-both-equal
          ( PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡t₂ t₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡
          )
  dec~↑-[]-cong-cong _ _ (no not-all-equal) _ _ =
    no λ (_ , bc~bc) →
    let _ , _ , _ , _ , _ , _ , bc≡bc , A₁≡ , _ , _ , v₁~ , _ =
          inv-[]-cong~ bc~bc
        s₁≡s₂ , ≡A₂ , _ , _ , ≡v₂ =
          []-cong-PE-injectivity (PE.sym bc≡bc)
    in
    not-all-equal
      ( s₁≡s₂
      , PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
      , _ , PE.subst (flip (_⊢_~_↓_ _ _) _) ≡v₂ v₁~
      )

private opaque

  -- A lemma used below.

  decConv↓-ΠΣ :
    ΠΣ-allowed b₁ p₁ q₁ →
    Dec
      (b₁ PE.≡ b₂ × p₁ PE.≡ p₂ × q₁ PE.≡ q₂ ×
       Γ ⊢ A₁ [conv↑] A₂) →
    (⊢ Γ ∙ A₁ ≡ Γ ∙ A₂ → Dec (Γ ∙ A₁ ⊢ B₁ [conv↑] B₂)) →
    Dec
      (Γ ⊢ ΠΣ⟨ b₁ ⟩ p₁ , q₁ ▷ A₁ ▹ B₁ [conv↓]
         ΠΣ⟨ b₂ ⟩ p₂ , q₂ ▷ A₂ ▹ B₂)
  decConv↓-ΠΣ ok (yes (PE.refl , PE.refl , PE.refl , A₁≡A₂)) dec =
    case dec (refl-∙ (soundnessConv↑ A₁≡A₂)) of λ where
      (yes B₁≡B₂) → yes (ΠΣ-cong A₁≡A₂ B₁≡B₂ ok)
      (no B₁≢B₂)  →
        no λ ΠΣ≡ΠΣ →
        let _ , _ , ΠΣ≡ΠΣ , _ , B₁≡ = inv-[conv↓]-ΠΣ ΠΣ≡ΠΣ
            _ , _ , _ , _ , ≡B₂     = ΠΣ-PE-injectivity (PE.sym ΠΣ≡ΠΣ)
        in
        B₁≢B₂ (PE.subst (_⊢_[conv↑]_ _ _) ≡B₂ B₁≡)
  decConv↓-ΠΣ _ (no not-all-equal) _ =
    no λ ΠΣ≡ΠΣ →
    let _ , _ , ΠΣ≡ΠΣ , A₁≡ , _         = inv-[conv↓]-ΠΣ ΠΣ≡ΠΣ
        b₁≡b₂ , p₁≡p₂ , q₁≡q₂ , ≡A₂ , _ =
          ΠΣ-PE-injectivity (PE.sym ΠΣ≡ΠΣ)
    in
    not-all-equal
      ( b₁≡b₂
      , p₁≡p₂
      , q₁≡q₂
      , PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡
      )

private opaque

  -- A lemma used below.

  decConv↓-Id :
    Dec (Γ ⊢ A₁ [conv↑] A₂) →
    (Γ ⊢ A₂ ≡ A₁ → Dec (Γ ⊢ t₁ [conv↑] t₂ ∷ A₁)) →
    (Γ ⊢ A₂ ≡ A₁ → Dec (Γ ⊢ u₁ [conv↑] u₂ ∷ A₁)) →
    Dec (Γ ⊢ Id A₁ t₁ u₁ [conv↓] Id A₂ t₂ u₂)
  decConv↓-Id (yes A₁≡A₂) dec₁ dec₂ =
    let A₂≡A₁ = _⊢_≡_.sym (soundnessConv↑ A₁≡A₂) in
    case dec₁ A₂≡A₁ ×-dec dec₂ A₂≡A₁ of λ where
      (yes (t₁≡t₂ , u₁≡u₂)) → yes (Id-cong A₁≡A₂ t₁≡t₂ u₁≡u₂)
      (no not-both-equal)   →
        no λ Id≡Id →
        let _ , _ , _ , Id≡Id , _ , t₁≡ , u₁≡ = inv-[conv↓]-Id Id≡Id
            _ , ≡t₂ , ≡u₂                     =
              Id-PE-injectivity (PE.sym Id≡Id)
        in
        not-both-equal
          ( PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡t₂ t₁≡
          , PE.subst (flip (_⊢_[conv↑]_∷_ _ _) _) ≡u₂ u₁≡
          )
  decConv↓-Id (no A₁≢A₂) _ _ =
    no λ Id≡Id →
    let _ , _ , _ , Id≡Id , A₁≡ , _ = inv-[conv↓]-Id Id≡Id
        ≡A₂ , _                     = Id-PE-injectivity (PE.sym Id≡Id)
    in
    A₁≢A₂ (PE.subst (_⊢_[conv↑]_ _ _) ≡A₂ A₁≡)

------------------------------------------------------------------------
-- Public definitions

mutual
  -- Decidability of algorithmic equality of neutrals.
  dec~↑ : ∀ {k l R T k′ l′}
        → Γ ⊢ k ~ k′ ↑ R → Γ ⊢ l ~ l′ ↑ T
        → Dec (∃ λ A → Γ ⊢ k ~ l ↑ A)
  dec~↑ (var-refl {x} ⊢x _) u~ = case inv-~-var u~ of λ where
    (inj₁ (y , PE.refl , _)) → case x ≟ⱽ y of λ where
      (yes x≡y) → yes (_ , var-refl ⊢x x≡y)
      (no x≢y)  → no (x≢y ∘→ var-PE-injectivity ∘→ inv-~var ∘→ proj₂)
    (inj₂ (u≢var , _)) → no (u≢var ∘→ (_ ,_) ∘→ inv-var~ ∘→ proj₂)
  dec~↑ (app-cong t₁~ t₂≡) u~ = case inv-~-∘ u~ of λ where
    (inj₁
       (_ , _ , _ , _ , _ , _ , _ , _ , _ ,
        PE.refl , _ , u₁~ , u₂≡)) →
      dec~↑-app-cong (~↓→∷ t₁~) (~↓→∷ u₁~) (dec~↓ t₁~ u₁~)
        (λ B₁≡C₁ → decConv↑TermConv B₁≡C₁ t₂≡ u₂≡)
    (inj₂ (u≢∘ , _)) →
      no λ (_ , t~u) →
      let _ , _ , _ , _ , _ , _ , u≡∘ , _ = inv-∘~ t~u in
      u≢∘ (_ , _ , _ , u≡∘)
  dec~↑ (fst-cong t′~) u~ = case inv-~-fst u~ of λ where
    (inj₁ (_ , _ , _ , _ , _ , PE.refl , _ , u′~)) →
      dec~↑-fst-cong (~↓→∷ t′~) (_ ≟ _ ×-dec dec~↓ t′~ u′~)
    (inj₂ (u≢fst , _)) →
      no λ (_ , t~u) →
      let _ , _ , _ , u≡fst , _ = inv-fst~ t~u in
      u≢fst (_ , _ , u≡fst)
  dec~↑ (snd-cong t′~) u~ = case inv-~-snd u~ of λ where
    (inj₁ (_ , _ , _ , _ , _ , _ , _ , PE.refl , _ , u′~)) →
      dec~↑-snd-cong (~↓→∷ t′~) (_ ≟ _ ×-dec dec~↓ t′~ u′~)
    (inj₂ (u≢snd , _)) →
      no λ (_ , t~u) →
      let _ , _ , _ , _ , _ , u≡snd , _ = inv-snd~ t~u in
      u≢snd (_ , _ , u≡snd)
  dec~↑ (prodrec-cong B≡ t₁~ t₂≡) u~ = case inv-~-prodrec u~ of λ where
    (inj₁
       (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ ,
        PE.refl , _ , C≡ , u₁~ , u₂≡)) →
      dec~↑-prodrec-cong (~↓→∷ t₁~) (~↓→∷ u₁~)
        (_ ≟ _ ×-dec _ ≟ _ ×-dec dec~↓ t₁~ u₁~)
        (λ eq → decConv↑′ eq B≡ C≡)
        (λ eq₁ eq₂ → decConv↑Term t₂≡ (convConv↑Term′ eq₁ eq₂ u₂≡))
    (inj₂ (u≢pr , _)) →
      no λ (_ , t~u) →
      let _ , _ , _ , _ , _ , _ , _ , u≡pr , _ = inv-prodrec~ t~u in
      u≢pr (_ , _ , _ , _ , _ , _ , u≡pr)
  dec~↑ (emptyrec-cong B≡ t′~) u~ = case inv-~-emptyrec u~ of λ where
    (inj₁ (_ , _ , _ , _ , PE.refl , _ , C≡ , u′~)) →
      dec~↑-emptyrec-cong (~↓→∷ t′~)
        (_ ≟ _ ×-dec decConv↑ B≡ C≡ ×-dec dec~↓ t′~ u′~)
    (inj₂ (u≢er , _)) →
      no λ (_ , t~u) →
      let _ , _ , _ , u≡er , _ = inv-emptyrec~ t~u in
      u≢er (_ , _ , _ , u≡er)
  dec~↑ (unitrec-cong B≡ t₁~ t₂≡ no-η) u~ =
    case inv-~-unitrec u~ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ ,
          PE.refl , _ , C≡ , u₁~ , u₂≡ , _)) →
        dec~↑-unitrec-cong no-η (~↓→∷ t₁~)
          (_ ≟ᵘ _ ×-dec _ ≟ _ ×-dec _ ≟ _ ×-dec dec~↓ t₁~ u₁~)
          (λ eq → decConv↑′ eq B≡ C≡)
          (λ eq → decConv↑TermConv eq t₂≡ u₂≡)
      (inj₂ (u≢ur , _)) →
        no λ (_ , t~u) →
        let _ , _ , _ , _ , u≡ur , _ = inv-unitrec~ t~u in
        u≢ur (_ , _ , _ , _ , _ , _ , u≡ur)
  dec~↑ (natrec-cong B≡ t₁≡ t₂≡ t₃~) u~ =
    case inv-~-natrec u~ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ ,
          PE.refl , _ , C≡ , u₁≡ , u₂≡ , u₃~)) →
        dec~↑-natrec-cong (~↓→∷ t₃~)
          (_ ≟ _ ×-dec _ ≟ _ ×-dec _ ≟ _ ×-dec decConv↑ B≡ C≡ ×-dec
           dec~↓ t₃~ u₃~)
          (λ eq → decConv↑TermConv eq t₁≡ u₁≡)
          (λ eq₁ eq₂ → decConv↑Term t₂≡ (convConv↑Term′ eq₁ eq₂ u₂≡))
      (inj₂ (u≢nr , _)) →
        no λ (_ , t~u) →
        let _ , _ , _ , _ , _ , u≡nr , _ = inv-natrec~ t~u in
        u≢nr (_ , _ , _ , _ , _ , _ , _ , u≡nr)
  dec~↑ (J-cong B₁≡ t₁≡ B₂≡ t₂≡ t₃≡ t₄~ B₃≡Id) u~ =
    case inv-~-J u~ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ ,
          _ , PE.refl , _ ,
          C₁≡ , u₁≡ , C₂≡ , u₂≡ , u₃≡ , u₄~ , _)) →
        dec~↑-J-cong (conv (~↓→∷ t₄~) B₃≡Id)
          (_ ≟ _ ×-dec _ ≟ _ ×-dec decConv↑ B₁≡ C₁≡ ×-dec dec~↓ t₄~ u₄~)
          (λ eq → decConv↑TermConv eq t₁≡ u₁≡)
          (λ eq → decConv↑′ eq B₂≡ C₂≡)
          (λ eq → decConv↑TermConv eq t₂≡ u₂≡)
          (λ eq → decConv↑TermConv eq t₃≡ u₃≡)
      (inj₂ (u≢J , _)) →
        no λ (_ , t~u) →
        let _ , _ , _ , _ , _ , _ , _ , _ , u≡J , _ = inv-J~ t~u in
        u≢J (_ , _ , _ , _ , _ , _ , _ , _ , u≡J)
  dec~↑ (K-cong B₁≡ t₁≡ B₂≡ t₂≡ t₃~ B₃≡Id ok) u~ =
    case inv-~-K u~ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ ,
          PE.refl , _ , C₁≡ , u₁≡ , C₂≡ , u₂≡ , u₃~ , _)) →
        dec~↑-K-cong ok (conv (~↓→∷ t₃~) B₃≡Id)
          (_ ≟ _ ×-dec decConv↑ B₁≡ C₁≡ ×-dec dec~↓ t₃~ u₃~)
          (λ eq → decConv↑TermConv eq t₁≡ u₁≡)
          (λ eq → decConv↑′ eq B₂≡ C₂≡)
          (λ eq → decConv↑TermConv eq t₂≡ u₂≡)
      (inj₂ (u≢K , _)) →
        no λ (_ , t~u) →
        let _ , _ , _ , _ , _ , _ , _ , u≡K , _ = inv-K~ t~u in
        u≢K (_ , _ , _ , _ , _ , _ , u≡K)
  dec~↑ ([]-cong-cong B₁≡ t₁≡ t₂≡ t₃~ B₂≡Id ok) u~ =
    case inv-~-[]-cong u~ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ ,
          PE.refl , _ , C₁≡ , u₁≡ , u₂≡ , u₃~ , _)) →
        dec~↑-[]-cong-cong ok (conv (~↓→∷ t₃~) B₂≡Id)
          (decStrength _ _ ×-dec decConv↑ B₁≡ C₁≡ ×-dec dec~↓ t₃~ u₃~)
          (λ eq → decConv↑TermConv eq t₁≡ u₁≡)
          (λ eq → decConv↑TermConv eq t₂≡ u₂≡)
      (inj₂ (u≢bc , _)) →
        no λ (_ , t~u) →
        let _ , _ , _ , _ , _ , _ , u≡bc , _ = inv-[]-cong~ t~u in
        u≢bc (_ , _ , _ , _ , _ , u≡bc)

  dec~↑′ : ∀ {k l R T}
        → ⊢ Γ ≡ Δ
        → Γ ⊢ k ~ k ↑ R → Δ ⊢ l ~ l ↑ T
        → Dec (∃ λ A → Γ ⊢ k ~ l ↑ A)
  dec~↑′ Γ≡Δ k~k l~l = dec~↑ k~k (stability~↑ (symConEq Γ≡Δ) l~l)

  -- Decidability of algorithmic equality of neutrals with types in WHNF.
  dec~↓ : ∀ {k l R T k′ l′}
        → Γ ⊢ k ~ k′ ↓ R → Γ ⊢ l ~ l′ ↓ T
        → Dec (∃ λ A → Γ ⊢ k ~ l ↓ A)
  dec~↓ ([~] _ _ k~l) ([~] _ _ k~l₁) with dec~↑ k~l k~l₁
  dec~↓ ([~] _ _ k~l) ([~] _ _ k~l₁) | yes (B , k~l₂) =
    let ⊢B , _ , _ = syntacticEqTerm (soundness~↑ k~l₂)
        C , whnfC , D′ = whNorm ⊢B
    in  yes (C , [~] B (D′ , whnfC) k~l₂)
  dec~↓ ([~] _ _ k~l) ([~] _ _ k~l₁) | no ¬p =
    no (λ { (_ , [~] A₃ _ k~l₂) → ¬p (A₃ , k~l₂) })

  -- Decidability of algorithmic equality of types.
  decConv↑ : ∀ {A B A′ B′}
           → Γ ⊢ A [conv↑] A′ → Γ ⊢ B [conv↑] B′
           → Dec (Γ ⊢ A [conv↑] B)
  decConv↑ ([↑] A′ B′ D D′ A′<>B′)
               ([↑] A″ B″ D₁ D″ A′<>B″)
           with decConv↓ A′<>B′ A′<>B″
  decConv↑ ([↑] A′ B′ D D′ A′<>B′)
               ([↑] A″ B″ D₁ D″ A′<>B″) | yes p =
    yes ([↑] A′ A″ D D₁ p)
  decConv↑ ([↑] A′ B′ D D′ A′<>B′)
               ([↑] A″ B″ D₁ D″ A′<>B″) | no ¬p =
    no (λ { ([↑] A‴ B‴ D₂ D‴ A′<>B‴) →
        let A‴≡B′ = whrDet* D₂ D
            B‴≡B″ = whrDet* D‴ D₁
        in  ¬p (PE.subst₂ (λ x y → _ ⊢ x [conv↓] y) A‴≡B′ B‴≡B″ A′<>B‴) })

  decConv↑′ : ∀ {A B A′ B′}
            → ⊢ Γ ≡ Δ
            → Γ ⊢ A [conv↑] A′ → Δ ⊢ B [conv↑] B′
            → Dec (Γ ⊢ A [conv↑] B)
  decConv↑′ Γ≡Δ A B = decConv↑ A (stabilityConv↑ (symConEq Γ≡Δ) B)

  -- Decidability of algorithmic equality of types in WHNF.
  decConv↓ : ∀ {A B A′ B′}
           → Γ ⊢ A [conv↓] A′ → Γ ⊢ B [conv↓] B′
           → Dec (Γ ⊢ A [conv↓] B)
  decConv↓ (ne A~) B≡ =
    let _ , A-ne , _ = ne~↓ A~ in
    case inv-[conv↓]-ne′ B≡ of λ where
      (inj₁ (_ , B~)) →
        case dec~↓ A~ B~ of λ where
          (yes (_ , A~B)) →
            yes $ ne $
            let C-whnf , _ = ne~↓ A~B
                U≡A′       = neTypeEq A-ne (~↓→∷ A~) (~↓→∷ A~B)
            in
            PE.subst (_⊢_~_↓_ _ _ _) (U≡A U≡A′ C-whnf) A~B
          (no ¬A~B) →
            no (¬A~B ∘→ (_ ,_) ∘→ proj₂ ∘→ inv-[conv↓]-ne A-ne)
      (inj₂ (¬-B-ne , _)) →
        no λ A≡B →
        ¬-B-ne (ne~↓ (inv-[conv↓]-ne A-ne A≡B .proj₂) .proj₂ .proj₂)
  decConv↓ U≡U@(U-refl {l = l₁} _) B≡ =
    case inv-[conv↓]-U′ B≡ of λ where
      (inj₁ (l₂ , PE.refl , _)) →
        case l₁ ≟ᵘ l₂ of λ where
          (yes PE.refl) → yes U≡U
          (no l₁≢l₂)    →
            no (l₁≢l₂ ∘→ U-injectivity ∘→
                soundnessConv↓
                  ⦃ no-equality-reflection = no-equality-reflection ⦄)
      (inj₂ (B≢U , _)) → no (B≢U ∘→ (_ ,_) ∘→ inv-[conv↓]-U)
  decConv↓ (ΠΣ-cong A₁≡ A₂≡ ok) B≡ =
    case inv-[conv↓]-ΠΣ′ B≡ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ , _ , PE.refl , PE.refl , B₁≡ , B₂≡)) →
        decConv↓-ΠΣ ok
          (decBinderMode _ _ ×-dec _ ≟ _ ×-dec _ ≟ _ ×-dec
           decConv↑ A₁≡ B₁≡)
          (λ eq → decConv↑′ eq A₂≡ B₂≡)
      (inj₂ (B≢ΠΣ , _)) →
        no λ ΠΣ≡B →
        let _ , _ , B≡ΠΣ , _ = inv-[conv↓]-ΠΣ ΠΣ≡B in
        B≢ΠΣ (_ , _ , _ , _ , _ , B≡ΠΣ)
  decConv↓ Empty≡Empty@(Empty-refl _) B≡ =
    case inv-[conv↓]-Empty′ B≡ of λ where
      (inj₁ (PE.refl , _)) → yes Empty≡Empty
      (inj₂ (B≢Empty , _)) → no (B≢Empty ∘→ inv-[conv↓]-Empty)
  decConv↓ Unit≡Unit@(Unit-refl {s = s} {l = l} _ _) B≡ =
    case inv-[conv↓]-Unit′ B≡ of λ where
      (inj₁ (s′ , l′ , PE.refl , _)) →
        case decStrength s s′ ×-dec l ≟ᵘ l′ of λ where
          (yes (PE.refl , PE.refl)) → yes Unit≡Unit
          (no not-both-equal)       →
            no λ Unit≡Unit →
            case inv-[conv↓]-Unit Unit≡Unit of λ {
              PE.refl →
            not-both-equal (PE.refl , PE.refl) }
      (inj₂ (B≢Unit , _)) →
        no λ Unit≡B → B≢Unit (_ , _ , inv-[conv↓]-Unit Unit≡B)
  decConv↓ ℕ≡ℕ@(ℕ-refl _) B≡ =
    case inv-[conv↓]-ℕ′ B≡ of λ where
      (inj₁ (PE.refl , _)) → yes ℕ≡ℕ
      (inj₂ (B≢ℕ , _))     → no (B≢ℕ ∘→ inv-[conv↓]-ℕ)
  decConv↓ (Id-cong A′≡ t₁≡ t₂≡) B≡ =
    case inv-[conv↓]-Id′ B≡ of λ where
      (inj₁
         (_ , _ , _ , _ , _ , _ ,
          PE.refl , PE.refl , B′≡ , u₁≡ , u₂≡)) →
        decConv↓-Id (decConv↑ A′≡ B′≡)
          (λ A′≡B′ → decConv↑Term t₁≡ (convConv↑Term A′≡B′ u₁≡))
          (λ A′≡B′ → decConv↑Term t₂≡ (convConv↑Term A′≡B′ u₂≡))
      (inj₂ (B≢Id , _)) →
        no λ Id≡B →
        let _ , _ , _ , B≡Id , _ = inv-[conv↓]-Id Id≡B in
        B≢Id (_ , _ , _ , B≡Id)

  -- Decidability of algorithmic equality of terms.
  decConv↑Term : ∀ {t u A t′ u′}
               → Γ ⊢ t [conv↑] t′ ∷ A → Γ ⊢ u [conv↑] u′ ∷ A
               → Dec (Γ ⊢ t [conv↑] u ∷ A)
  decConv↑Term ([↑]ₜ B t′ u′ D d d′ t<>u)
               ([↑]ₜ B₁ t″ u″ D₁ d₁ d″ t<>u₁)
               rewrite whrDet* D D₁
                 with decConv↓Term t<>u t<>u₁
  decConv↑Term ([↑]ₜ B t′ u′ D d d′ t<>u)
               ([↑]ₜ B₁ t″ u″ D₁ d₁ d″ t<>u₁)
               | yes p = yes ([↑]ₜ B₁ t′ t″ D₁ d d₁ p)
  decConv↑Term ([↑]ₜ B t′ u′ D d d′ t<>u)
               ([↑]ₜ B₁ t″ u″ D₁ d₁ d″ t<>u₁)
               | no ¬p =
    no (λ { ([↑]ₜ B₂ t‴ u‴ D₂ d₂ d‴ t<>u₂) →
        let B₂≡B₁ = whrDet* D₂ D₁
            t‴≡u′ = whrDet*Term d₂
                      (PE.subst (_⊢_↘_∷_ _ _ _) (PE.sym B₂≡B₁) d)
            u‴≡u″ = whrDet*Term d‴
                      (PE.subst (_⊢_↘_∷_ _ _ _) (PE.sym B₂≡B₁) d₁)
        in  ¬p (PE.subst₃ (λ x y z → _ ⊢ x [conv↓] y ∷ z)
                          t‴≡u′ u‴≡u″ B₂≡B₁ t<>u₂)})

  decConv↑Term′ : ∀ {t u A}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ t [conv↑] t ∷ A → Δ ⊢ u [conv↑] u ∷ A
                → Dec (Γ ⊢ t [conv↑] u ∷ A)
  decConv↑Term′ Γ≡Δ t u = decConv↑Term t (stabilityConv↑Term (symConEq Γ≡Δ) u)

  -- Decidability of algorithmic equality of terms in WHNF.
  decConv↓Term : ∀ {t u A t′ u′}
               → Γ ⊢ t [conv↓] t′ ∷ A → Γ ⊢ u [conv↓] u′ ∷ A
               → Dec (Γ ⊢ t [conv↓] u ∷ A)
  decConv↓Term (ne-ins ⊢t _ A-ne t~) u≡ =
    let _ , u~ = inv-[conv↓]∷-ne A-ne u≡ in
    case dec~↓ t~ u~ of λ where
      (yes (_ , t~u)) → yes (ne-ins ⊢t ([conv↓]∷→∷ u≡) A-ne t~u)
      (no ¬t~u)       → no (¬t~u ∘→ inv-[conv↓]∷-ne A-ne)
  decConv↓Term (univ ⊢A _ A≡) B≡ =
    case decConv↓ A≡ (inv-[conv↓]∷-U B≡) of λ where
      (yes A≡B) → yes (univ ⊢A ([conv↓]∷→∷ B≡) A≡B)
      (no A≢B)  → no (A≢B ∘→ inv-[conv↓]∷-U)
  decConv↓Term (η-eq ⊢t _ t-fun _ t0≡) u≡ =
    let u-fun , _ , u0≡ = inv-[conv↓]∷-Π u≡ in
    case decConv↑Term t0≡ u0≡ of λ where
      (yes t0≡u0) → yes (η-eq ⊢t ([conv↓]∷→∷ u≡) t-fun u-fun t0≡u0)
      (no t0≢u0)  →
        no λ t≡u →
        let _ , _ , t0≡u0 = inv-[conv↓]∷-Π t≡u in
        t0≢u0 t0≡u0
  decConv↓Term (Σ-η ⊢t _ t-prod _ fst-t≡ snd-t≡) u≡ =
    let u-prod , _ , fst-u≡ , snd-u≡ = inv-[conv↓]∷-Σˢ u≡ in
    case
      (decConv↑Term fst-t≡ fst-u≡
         ×-dec′ λ fst-t≡fst-u →
       decConv↑TermConv
         (substTypeEq
            (refl (inversion-ΠΣ (syntacticTerm ⊢t) .proj₂ .proj₁))
            (soundnessConv↑Term fst-t≡fst-u))
         snd-t≡ snd-u≡)
      of λ where
      (yes (fst-t≡fst-u , snd-t≡snd-u)) →
        yes $
        Σ-η ⊢t ([conv↓]∷→∷ u≡) t-prod u-prod fst-t≡fst-u snd-t≡snd-u
      (no not-both-equal) →
        no λ t≡u →
        let _ , _ , fst-t≡fst-u , snd-t≡snd-u = inv-[conv↓]∷-Σˢ t≡u in
        not-both-equal (fst-t≡fst-u , snd-t≡snd-u)
  decConv↓Term (Σʷ-ins ⊢t _ t~) u≡ = case inv-[conv↓]∷-Σʷ u≡ of λ where
    (inj₁ (_ , _ , _ , _ , u~)) →
      case dec~↓ t~ u~ of λ where
        (yes (_ , t~u)) →
          yes $
          Σʷ-ins ⊢t ([conv↓]∷→∷ u≡) $
          PE.subst (_⊢_~_↓_ _ _ _)
            (uncurry Σ≡A (~↓→∷→Whnf×≡ t~u ⊢t) .proj₂ .proj₂) t~u
        (no ¬t~u) → no (¬t~u ∘→ [conv↓]∷Σʷ→~↓ t~)
    (inj₂ (_ , _ , _ , _ , PE.refl , _)) →
      no λ t≡prod →
      let _ , [~] _ _ ~prod = [conv↓]∷Σʷ→~↓ t~ t≡prod in
      inv-~prod ~prod
  decConv↓Term (prod-cong ⊢B t₁≡ t₂≡ ok) u≡ =
    case inv-[conv↓]∷-Σʷ u≡ of λ where
      (inj₁ (_ , _ , _ , _ , u~)) →
        no λ prod≡u →
        let _ , [~] _ _ ~prod =
              [conv↓]∷Σʷ→~↓ u~ (symConv↓Term′ prod≡u)
        in
        inv-~prod ~prod
      (inj₂ (_ , _ , _ , _ , PE.refl , _ , u₁≡ , u₂≡)) →
        case
          (decConv↑Term t₁≡ u₁≡
             ×-dec′ λ t₁≡u₁ →
           decConv↑TermConv
             (substTypeEq (refl ⊢B) (soundnessConv↑Term t₁≡u₁))
             t₂≡ u₂≡)
          of λ where
          (yes (t₁≡u₁ , t₂≡u₂)) → yes (prod-cong ⊢B t₁≡u₁ t₂≡u₂ ok)
          (no not-both-equal)   →
            no λ t≡u →
            let _ , _ , _ , t₁≡u₁ , t₂≡u₂ , _ = prod-cong⁻¹ t≡u in
            not-both-equal (t₁≡u₁ , t₂≡u₂)
  decConv↓Term (Empty-ins t~) u≡ =
    case dec~↓ t~ (inv-[conv↓]∷-Empty u≡) of λ where
      (yes (_ , t~u)) →
        yes $ Empty-ins $
        PE.subst (_⊢_~_↓_ _ _ _)
          (uncurry Empty≡A (~↓→∷→Whnf×≡ t~u (~↓→∷ t~))) t~u
      (no ¬t~u) → no (¬t~u ∘→ (_ ,_) ∘→ inv-[conv↓]∷-Empty)
  decConv↓Term (Unitʷ-ins no-η t~) u≡ =
    case inv-[conv↓]∷-Unitʷ u≡ of λ where
      (inj₁ (_ , inj₁ u~)) → case dec~↓ t~ u~ of λ where
        (yes (_ , t~u)) →
          yes $ Unitʷ-ins no-η $
          PE.subst (_⊢_~_↓_ _ _ _)
            (uncurry Unit≡A (~↓→∷→Whnf×≡ t~u (~↓→∷ t~))) t~u
        (no ¬t~u) →
          no λ t≡u →
          case inv-[conv↓]∷-Unitʷ t≡u of λ where
            (inj₁ (_ , inj₁ t~u))           → ¬t~u (_ , t~u)
            (inj₁ (_ , inj₂ (PE.refl , _))) →
              let [~] _ _ t~ = t~ in
              inv-star~ t~
            (inj₂ (η , _)) → no-η η
      (inj₁ (_ , inj₂ (PE.refl , _))) →
        no (no-η ∘→ ≡starʷ→~↓Unitʷ→Unitʷ-η t~)
      (inj₂ (η , _)) → ⊥-elim (no-η η)
  decConv↓Term (η-unit ⊢t _ t-whnf _ η) u≡ =
    case inv-[conv↓]∷-Unit u≡ of λ where
      (inj₁ (η , u-whnf , _)) →
        yes (η-unit ⊢t ([conv↓]∷→∷ u≡) t-whnf u-whnf η)
      (inj₂ (no-η , _)) → ⊥-elim (no-η η)
  decConv↓Term star≡star@(starʷ-refl _ _ no-η) u≡ =
    case inv-[conv↓]∷-Unitʷ u≡ of λ where
      (inj₁ (_ , inj₂ (PE.refl , _))) → yes star≡star
      (inj₁ (_ , inj₁ u~))            →
        no (no-η ∘→ ≡starʷ→~↓Unitʷ→Unitʷ-η u~ ∘→ symConv↓Term′)
      (inj₂ (η , _)) → ⊥-elim (no-η η)
  decConv↓Term (ℕ-ins t~) u≡ = case inv-[conv↓]∷-ℕ u≡ of λ where
    (inj₁ u~) → case dec~↓ t~ u~ of λ where
      (yes (A , t~u)) →
        yes $ ℕ-ins $
        PE.subst (_⊢_~_↓_ _ _ _)
          (uncurry ℕ≡A (~↓→∷→Whnf×≡ t~u (~↓→∷ t~))) t~u
      (no ¬t~u) → no (¬t~u ∘→ (_ ,_) ∘→ [conv↓]∷ℕ→~↓ℕ t~)
    (inj₂ (inj₁ (PE.refl , _))) →
      no λ t≡zero →
      let [~] _ _ ~zero = [conv↓]∷ℕ→~↓ℕ t~ t≡zero in
      inv-~zero ~zero
    (inj₂ (inj₂ (_ , _ , PE.refl , _))) →
      no λ t≡suc →
      let [~] _ _ ~suc = [conv↓]∷ℕ→~↓ℕ t~ t≡suc in
      inv-~suc ~suc
  decConv↓Term zero≡zero@(zero-refl _) u≡ =
    case inv-[conv↓]∷-ℕ u≡ of λ where
      (inj₁ u~) →
        no λ zero≡t →
        let [~] _ _ ~zero = [conv↓]∷ℕ→~↓ℕ u~ (symConv↓Term′ zero≡t) in
        inv-~zero ~zero
      (inj₂ (inj₁ (PE.refl , _)))         → yes zero≡zero
      (inj₂ (inj₂ (_ , _ , PE.refl , _))) →
        no λ zero≡suc →
        case inv-[conv↓]∷-ℕ zero≡suc of λ where
          (inj₁ ([~] _ _ zero~suc))      → inv-zero~ zero~suc
          (inj₂ (inj₁ (_ , ())))
          (inj₂ (inj₂ (_ , _ , () , _)))
  decConv↓Term (suc-cong t≡) u≡ = case inv-[conv↓]∷-ℕ u≡ of λ where
    (inj₁ u~) →
      no λ suc≡t →
      let [~] _ _ ~suc = [conv↓]∷ℕ→~↓ℕ u~ (symConv↓Term′ suc≡t) in
      inv-~suc ~suc
    (inj₂ (inj₁ (PE.refl , _))) →
      no λ suc≡zero →
      case inv-[conv↓]∷-ℕ suc≡zero of λ where
        (inj₁ ([~] _ _ suc~zero))          → inv-~zero suc~zero
        (inj₂ (inj₁ (() , _)))
        (inj₂ (inj₂ (_ , _ , _ , () , _)))
    (inj₂ (inj₂ (_ , _ , PE.refl , _ , u≡))) →
      case decConv↑Term t≡ u≡ of λ where
        (yes t≡u) → yes (suc-cong t≡u)
        (no t≢u)  →
          no λ suc-t≡suc-u →
          case inv-[conv↓]∷-ℕ suc-t≡suc-u of λ where
            (inj₁ ([~] _ _ suc~suc)) →
              inv-suc~ suc~suc
            (inj₂ (inj₁ (() , _)))
            (inj₂ (inj₂ (_ , _ , PE.refl , PE.refl , t≡u))) →
              t≢u t≡u
  decConv↓Term (Id-ins ⊢t t~) u≡ = case inv-[conv↓]∷-Id u≡ of λ where
    (inj₁ (_ , _ , _ , u~)) →
      case dec~↓ t~ u~ of λ where
        (yes (_ , t~u)) →
          yes $
          Id-ins ⊢t $
          PE.subst (_⊢_~_↓_ _ _ _)
            (uncurry Id≡Whnf (~↓→∷→Whnf×≡ t~u (~↓→∷ t~))
               .proj₂ .proj₂ .proj₂)
            t~u
        (no ¬t~u) →
          no λ t≡u →
          case inv-[conv↓]∷-Id t≡u of λ where
            (inj₁ (_ , _ , _ , t~u)) → ¬t~u (_ , t~u)
            (inj₂ (_ , PE.refl , _)) →
              let [~] _ _ rfl~ = u~ in
              inv-rfl~ rfl~
    (inj₂ (PE.refl , _)) →
      no λ rfl≡u →
      ¬-Neutral-rfl $
      case inv-[conv↓]∷-Id rfl≡u of λ where
        (inj₁ (_ , _ , _ , t~rfl)) → ne~↓ t~rfl .proj₂ .proj₂
        (inj₂ (PE.refl , _))       → ne~↓ t~ .proj₂ .proj₁
  decConv↓Term rfl≡rfl@(rfl-refl _) u≡ =
    case inv-[conv↓]∷-Id u≡ of λ where
      (inj₁ (_ , _ , _ , u~)) →
        no λ rfl≡u →
        ¬-Neutral-rfl $
        case inv-[conv↓]∷-Id rfl≡u of λ where
          (inj₁ (_ , _ , _ , rfl~u)) → ne~↓ rfl~u .proj₂ .proj₁
          (inj₂ (_ , PE.refl , _))   → ne~↓ u~ .proj₂ .proj₁
      (inj₂ (PE.refl , _)) → yes rfl≡rfl

  -- Decidability of algorithmic equality of terms of equal types.
  decConv↑TermConv : ∀ {t u A B t′ u′}
                → Γ ⊢ A ≡ B
                → Γ ⊢ t [conv↑] t′ ∷ A
                → Γ ⊢ u [conv↑] u′ ∷ B
                → Dec (Γ ⊢ t [conv↑] u ∷ A)
  decConv↑TermConv A≡B t u =
    decConv↑Term t (convConv↑Term (sym A≡B) u)