------------------------------------------------------------------------
-- Terms blocked on variables and opaque definitions.
------------------------------------------------------------------------

open import Definition.Typed.Variant

module Definition.Untyped.Neutral
  {a} (M : Set a)
  (type-variant : Type-variant a)
  where

open Type-variant type-variant

open import Definition.Untyped M
open import Definition.Untyped.Inversion M

open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Level as L using (module Lift)
open import Tools.Nat
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum renaming (map to ⊎-map)
open import Tools.Unit

private variable
  α m n             : Nat
  x                 : Fin _
  y                 : Nat ⊎ Fin _
  V V′              : Set a
  ∇                 : DCon (Term ) _
  A B C F G t u v w : Term _
  l                 : Lvl _
  s                 : Strength
  b                 : BinderMode
  p q r             : M

------------------------------------------------------------------------
-- Neutral terms

-- A term is neutral if reduction is blocked by a variable or an
-- opaque definition in its head position.
--
-- If quotient types are allowed but equality reflection is not
-- allowed, then applications of resp and set are also treated as
-- neutral.

data Neutral {m n} (V : Set a) (∇ : DCon (Term ) m) : Term n → Set a where
  defn      : α ↦⊘∷ A ∈ ∇   → Neutral V ∇ (defn α)
  var       : V → ∀ x       → Neutral V ∇ (var x)
  supᵘˡₙ    : Neutral V ∇ t → Neutral V ∇ (t supᵘ u)
  supᵘʳₙ    : Neutral V ∇ u → Neutral V ∇ (sucᵘ t supᵘ u)
  lowerₙ    : Neutral V ∇ t → Neutral V ∇ (lower t)
  ∘ₙ        : Neutral V ∇ t → Neutral V ∇ (t ∘⟨ p ⟩ u)
  fstₙ      : Neutral V ∇ t → Neutral V ∇ (fst p t)
  sndₙ      : Neutral V ∇ t → Neutral V ∇ (snd p t)
  natrecₙ   : Neutral V ∇ v → Neutral V ∇ (natrec p q r G t u v)
  prodrecₙ  : Neutral V ∇ t → Neutral V ∇ (prodrec r p q A t u)
  emptyrecₙ : Neutral V ∇ t → Neutral V ∇ (emptyrec p A t)
  unitrecₙ  : ¬ Unitʷ-η →
              Neutral V ∇ t → Neutral V ∇ (unitrec p q A t u)
  Jₙ        : Neutral V ∇ w → Neutral V ∇ (J p q A t B u v w)
  Kₙ        : Neutral V ∇ v → Neutral V ∇ (K p A t B u v)
  []-congₙ  : Neutral V ∇ v → Neutral V ∇ ([]-cong s l A t u v)
  resp      : Higher-quotient-constructors-neutral →
              Neutral V ∇ (resp A B t u v)
  set       : Higher-quotient-constructors-neutral →
              Neutral V ∇ (set A B t u v w)
  qrec      : Neutral V ∇ w → Neutral V ∇ (qrec C t u v w)

opaque

  ne→ : (V → V′) → Neutral V ∇ t → Neutral V′ ∇ t
  ne→ f (defn α↦⊘)     = defn α↦⊘
  ne→ f (var ok x)     = var (f ok) x
  ne→ f (supᵘˡₙ b)     = supᵘˡₙ (ne→ f b)
  ne→ f (supᵘʳₙ b)     = supᵘʳₙ (ne→ f b)
  ne→ f (lowerₙ b)     = lowerₙ (ne→ f b)
  ne→ f (∘ₙ b)         = ∘ₙ (ne→ f b)
  ne→ f (fstₙ b)       = fstₙ (ne→ f b)
  ne→ f (sndₙ b)       = sndₙ (ne→ f b)
  ne→ f (natrecₙ b)    = natrecₙ (ne→ f b)
  ne→ f (prodrecₙ b)   = prodrecₙ (ne→ f b)
  ne→ f (emptyrecₙ b)  = emptyrecₙ (ne→ f b)
  ne→ f (unitrecₙ u b) = unitrecₙ u (ne→ f b)
  ne→ f (Jₙ b)         = Jₙ (ne→ f b)
  ne→ f (Kₙ b)         = Kₙ (ne→ f b)
  ne→ f ([]-congₙ b)   = []-congₙ (ne→ f b)
  ne→ f (resp ok)      = resp ok
  ne→ f (set ok)       = set ok
  ne→ f (qrec n)       = qrec (ne→ f n)

opaque

  ne↑ : V → Neutral V′ ∇ t → Neutral V ∇ t
  ne↑ ok = ne→ (λ _ → ok)

------------------------------------------------------------------------
-- Constructor applications are not neutral

opaque

  -- Constructor applications are not neutral.

  ¬-Neutral-Level : ¬ Neutral {n = n} V ∇ Level
  ¬-Neutral-Level ()

  ¬-Neutral-U : ¬ Neutral {n = n} V ∇ (U l)
  ¬-Neutral-U ()

  ¬-Neutral-Lift : ¬ Neutral {n = n} V ∇ (Lift l A)
  ¬-Neutral-Lift ()

  ¬-Neutral-ΠΣ : ¬ Neutral V ∇ (ΠΣ⟨ b ⟩ p , q ▷ A ▹ B)
  ¬-Neutral-ΠΣ ()

  ¬-Neutral-lam : ¬ Neutral V ∇ (lam p t)
  ¬-Neutral-lam ()

  ¬-Neutral-prod : ¬ Neutral V ∇ (prod s p t u)
  ¬-Neutral-prod ()

  ¬-Neutral-Empty : ¬ Neutral {n = n} V ∇ Empty
  ¬-Neutral-Empty ()

  ¬-Neutral-Unit : ¬ Neutral {n = n} V ∇ (Unit s)
  ¬-Neutral-Unit ()

  ¬-Neutral-star : ¬ Neutral {n = n} V ∇ (star s)
  ¬-Neutral-star ()

  ¬-Neutral-ℕ : ¬ Neutral {n = n} V ∇ ℕ
  ¬-Neutral-ℕ ()

  ¬-Neutral-zero : ¬ Neutral {n = n} V ∇ zero
  ¬-Neutral-zero ()

  ¬-Neutral-suc : ¬ Neutral V ∇ (suc t)
  ¬-Neutral-suc ()

  ¬-Neutral-Id : ¬ Neutral V ∇ (Id A t u)
  ¬-Neutral-Id ()

  ¬-Neutral-rfl : ¬ Neutral {n = n} V ∇ rfl
  ¬-Neutral-rfl ()

  ¬-Neutral-Quot : ¬ Neutral V ∇ (Quot A B)
  ¬-Neutral-Quot ()

  ¬-Neutral-class : ¬ Neutral V ∇ (class t)
  ¬-Neutral-class ()

opaque

  -- Level literals are not neutral.

  ¬-Neutral-Level-literal :
    Level-literal t → ¬ Neutral V ∇ t
  ¬-Neutral-Level-literal zeroᵘ    ()
  ¬-Neutral-Level-literal (sucᵘ _) ()

------------------------------------------------------------------------
-- No-confusion lemmas

-- Different whnfs are trivially distinguished by propositional equality.
-- (The following statements are sometimes called "no-confusion theorems".)

opaque

  Level≢ne : Neutral V ∇ A → Level ≢ A
  Level≢ne () refl

opaque

  Lift≢ne : Neutral V ∇ A → Lift l B ≢ A
  Lift≢ne () refl

opaque

  U≢ne : Neutral V ∇ A → U l ≢ A
  U≢ne () refl

opaque

  ℕ≢ne : Neutral V ∇ A → ℕ ≢ A
  ℕ≢ne () refl

opaque

  Empty≢ne : Neutral V ∇ A → Empty ≢ A
  Empty≢ne () refl

opaque

  Unit≢ne : Neutral V ∇ A → Unit s ≢ A
  Unit≢ne () refl

opaque

  B≢ne : ∀ W → Neutral V ∇ A → ⟦ W ⟧ F ▹ G ≢ A
  B≢ne (BΠ p q)   () refl
  B≢ne (BΣ m p q) () refl

opaque

  ΠΣ≢ne : ∀ b → Neutral V ∇ A → ΠΣ⟨ b ⟩ p , q ▷ F ▹ G ≢ A
  ΠΣ≢ne BMΠ     () refl
  ΠΣ≢ne (BMΣ s) () refl

opaque

  Id≢ne : Neutral V ∇ B → Id A t u ≢ B
  Id≢ne () refl

opaque

  Quot≢ne : Neutral V ∇ C → Quot A B ≢ C
  Quot≢ne () refl

opaque

  zeroᵘ≢ne : Neutral V ∇ t → zeroᵘ ≢ t
  zeroᵘ≢ne () refl

opaque

  sucᵘ≢ne : Neutral V ∇ t → sucᵘ u ≢ t
  sucᵘ≢ne () refl

opaque

  zero≢ne : Neutral V ∇ t → zero ≢ t
  zero≢ne () refl

opaque

  suc≢ne : Neutral V ∇ t → suc u ≢ t
  suc≢ne () refl

opaque

  prod≢ne : ∀ {m} → Neutral V ∇ v → prod m p t u ≢ v
  prod≢ne () refl

opaque

  rfl≢ne : Neutral V ∇ t → rfl ≢ t
  rfl≢ne () refl

opaque

  star≢ne : Neutral V ∇ t → star s ≢ t
  star≢ne () refl

opaque

  class≢ne : Neutral V ∇ t → class u ≢ t
  class≢ne () refl

------------------------------------------------------------------------
-- Weakening

-- Weakening of a neutral term.

wkNeutral : ∀ ρ → Neutral V ∇ t → Neutral {n = n} V ∇ (wk ρ t)
wkNeutral ρ (var ok x)        = var ok (wkVar ρ x)
wkNeutral ρ (defn α↦⊘)        = defn α↦⊘
wkNeutral ρ (supᵘˡₙ t)        = supᵘˡₙ (wkNeutral ρ t)
wkNeutral ρ (supᵘʳₙ t)        = supᵘʳₙ (wkNeutral ρ t)
wkNeutral ρ (lowerₙ n)        = lowerₙ (wkNeutral ρ n)
wkNeutral ρ (∘ₙ b)            = ∘ₙ (wkNeutral ρ b)
wkNeutral ρ (fstₙ b)          = fstₙ (wkNeutral ρ b)
wkNeutral ρ (sndₙ b)          = sndₙ (wkNeutral ρ b)
wkNeutral ρ (natrecₙ b)       = natrecₙ (wkNeutral ρ b)
wkNeutral ρ (prodrecₙ b)      = prodrecₙ (wkNeutral ρ b)
wkNeutral ρ (emptyrecₙ b)     = emptyrecₙ (wkNeutral ρ b)
wkNeutral ρ (unitrecₙ no-η b) = unitrecₙ no-η (wkNeutral ρ b)
wkNeutral ρ (Jₙ b)            = Jₙ (wkNeutral ρ b)
wkNeutral ρ (Kₙ b)            = Kₙ (wkNeutral ρ b)
wkNeutral ρ ([]-congₙ b)      = []-congₙ (wkNeutral ρ b)
wkNeutral ρ (resp ok)         = resp ok
wkNeutral ρ (set ok)          = set ok
wkNeutral ρ (qrec n)          = qrec (wkNeutral ρ n)

------------------------------------------------------------------------
-- Inversion lemmas for Neutral

opaque

  -- An inversion lemma for supᵘ.

  inv-ne-supᵘ :
    Neutral V ∇ (t supᵘ u) →
    Neutral V ∇ t ⊎
    (∃ λ t′ → t ≡ sucᵘ t′ × Neutral V ∇ u)
  inv-ne-supᵘ (supᵘˡₙ n) = inj₁ n
  inv-ne-supᵘ (supᵘʳₙ n) = inj₂ (_ , refl , n)

opaque

  -- An inversion lemma for lower.

  inv-ne-lower : Neutral V ∇ (lower t) → Neutral V ∇ t
  inv-ne-lower (lowerₙ n) = n

opaque

  -- An inversion lemma for _∘⟨_⟩_.

  inv-ne-∘ : Neutral V ∇ (t ∘⟨ p ⟩ u) → Neutral V ∇ t
  inv-ne-∘ (∘ₙ b) = b

opaque

  -- An inversion lemma for fst.

  inv-ne-fst : Neutral V ∇ (fst p t) → Neutral V ∇ t
  inv-ne-fst (fstₙ b) = b

opaque

  -- An inversion lemma for snd.

  inv-ne-snd : Neutral V ∇ (snd p t) → Neutral V ∇ t
  inv-ne-snd (sndₙ b) = b

opaque

  -- An inversion lemma for natrec.

  inv-ne-natrec : Neutral V ∇ (natrec p q r A t u v) → Neutral V ∇ v
  inv-ne-natrec (natrecₙ b) = b

opaque

  -- An inversion lemma for prodrec.

  inv-ne-prodrec : Neutral V ∇ (prodrec r p q A t u) → Neutral V ∇ t
  inv-ne-prodrec (prodrecₙ b) = b

opaque

  -- An inversion lemma for emptyrec.

  inv-ne-emptyrec : Neutral V ∇ (emptyrec p A t) → Neutral V ∇ t
  inv-ne-emptyrec (emptyrecₙ b) = b

opaque

  -- An inversion lemma for unitrec.

  inv-ne-unitrec :
    Neutral V ∇ (unitrec p q A t u) → ¬ Unitʷ-η × Neutral V ∇ t
  inv-ne-unitrec (unitrecₙ no-η b) = no-η , b

opaque

  -- An inversion lemma for J.

  inv-ne-J : Neutral V ∇ (J p q A t B u v w) → Neutral V ∇ w
  inv-ne-J (Jₙ b) = b

opaque

  -- An inversion lemma for K.

  inv-ne-K : Neutral V ∇ (K p A t B u v) → Neutral V ∇ v
  inv-ne-K (Kₙ b) = b

opaque

  -- An inversion lemma for []-cong.

  inv-ne-[]-cong : Neutral V ∇ ([]-cong s l A t u v) → Neutral V ∇ v
  inv-ne-[]-cong ([]-congₙ b) = b

opaque

  -- An inversion lemma for resp.

  inv-ne-resp :
    Neutral V ∇ (resp A B t u v) → Higher-quotient-constructors-neutral
  inv-ne-resp (resp ok) = ok

opaque

  -- An inversion lemma for set.

  inv-ne-set :
    Neutral V ∇ (set A B t u v w) → Higher-quotient-constructors-neutral
  inv-ne-set (set ok) = ok

opaque

  -- An inversion lemma for qrec.

  inv-ne-qrec : Neutral V ∇ (qrec C t u v w) → Neutral V ∇ w
  inv-ne-qrec (qrec n) = n

------------------------------------------------------------------------
-- Specializations

Neutral⁺ : DCon (Term ) m → Term n → Set a
Neutral⁺ ∇ t = Neutral (L.Lift _ ⊤) ∇ t

opaque

  defn⁺ : α ↦⊘∷ A ∈ ∇ → Neutral⁺ {n = n} ∇ (defn α)
  defn⁺ = defn

opaque

  var⁺ : ∀ x → Neutral⁺ {n = n} ∇ (var x)
  var⁺ = var (L.lift tt)

opaque

  ne↑⁺ : Neutral V ∇ t → Neutral⁺ ∇ t
  ne↑⁺ = ne↑ (L.lift tt)

Neutral⁻ : DCon (Term ) m → Term n → Set a
Neutral⁻ ∇ t = Neutral (L.Lift _ ⊥) ∇ t

opaque

  defn⁻ : α ↦⊘∷ A ∈ ∇ → Neutral⁻ {n = n} ∇ (defn α)
  defn⁻ = defn

opaque

  ne→⁻ : Neutral⁻ ∇ t → Neutral V ∇ t
  ne→⁻ = ne→ (⊥-elim ∘→ Lift.lower)

opaque

  dichotomy-ne : Neutral V ∇ t → Neutral⁻ ∇ t ⊎ V
  dichotomy-ne (defn α↦⊘)        = inj₁ (defn α↦⊘)
  dichotomy-ne (var ok x)        = inj₂ ok
  dichotomy-ne (supᵘˡₙ b)        = ⊎-map supᵘˡₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (supᵘʳₙ b)        = ⊎-map supᵘʳₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (lowerₙ b)        = ⊎-map lowerₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (∘ₙ b)            = ⊎-map ∘ₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (fstₙ b)          = ⊎-map fstₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (sndₙ b)          = ⊎-map sndₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (natrecₙ b)       = ⊎-map natrecₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (prodrecₙ b)      = ⊎-map prodrecₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (emptyrecₙ b)     = ⊎-map emptyrecₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (unitrecₙ no-η b) = ⊎-map (unitrecₙ no-η) idᶠ (dichotomy-ne b)
  dichotomy-ne (Jₙ b)            = ⊎-map Jₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (Kₙ b)            = ⊎-map Kₙ idᶠ (dichotomy-ne b)
  dichotomy-ne ([]-congₙ b)      = ⊎-map []-congₙ idᶠ (dichotomy-ne b)
  dichotomy-ne (resp ok)         = inj₁ (resp ok)
  dichotomy-ne (set ok)          = inj₁ (set ok)
  dichotomy-ne (qrec n)          = ⊎-map qrec idᶠ (dichotomy-ne n)

opaque

  closed-ne : {t : Term } → Neutral V ∇ t → Neutral⁻ ∇ t
  closed-ne (defn α↦⊘)        = defn α↦⊘
  closed-ne (var _ ())
  closed-ne (supᵘˡₙ b)        = supᵘˡₙ (closed-ne b)
  closed-ne (supᵘʳₙ b)        = supᵘʳₙ (closed-ne b)
  closed-ne (lowerₙ b)        = lowerₙ (closed-ne b)
  closed-ne (∘ₙ b)            = ∘ₙ (closed-ne b)
  closed-ne (fstₙ b)          = fstₙ (closed-ne b)
  closed-ne (sndₙ b)          = sndₙ (closed-ne b)
  closed-ne (natrecₙ b)       = natrecₙ (closed-ne b)
  closed-ne (prodrecₙ b)      = prodrecₙ (closed-ne b)
  closed-ne (emptyrecₙ b)     = emptyrecₙ (closed-ne b)
  closed-ne (unitrecₙ no-η b) = unitrecₙ no-η (closed-ne b)
  closed-ne (Jₙ b)            = Jₙ (closed-ne b)
  closed-ne (Kₙ b)            = Kₙ (closed-ne b)
  closed-ne ([]-congₙ b)      = []-congₙ (closed-ne b)
  closed-ne (resp ok)         = resp ok
  closed-ne (set ok)          = set ok
  closed-ne (qrec n)          = qrec (closed-ne n)

------------------------------------------------------------------------
-- Another lemma

opaque

  -- If t is V′-neutral and the context is empty or V holds, then t is
  -- V-neutral.

  or-empty-Neutral :
    {Γ : Con Term n} {t : Term n} →
    ⦃ ok : V or-empty Γ ⦄ →
    Neutral V′ ∇ t → Neutral V ∇ t
  or-empty-Neutral ⦃ ok = ε ⦄ (var _ ())
  or-empty-Neutral ⦃ ok = possibly-nonempty ⦃ ok ⦄ ⦄ (var _ _) =
    var ok _
  or-empty-Neutral (defn ∈∇)         = defn ∈∇
  or-empty-Neutral (supᵘˡₙ n)        = supᵘˡₙ (or-empty-Neutral n)
  or-empty-Neutral (supᵘʳₙ n)        = supᵘʳₙ (or-empty-Neutral n)
  or-empty-Neutral (lowerₙ n)        = lowerₙ (or-empty-Neutral n)
  or-empty-Neutral (∘ₙ n)            = ∘ₙ (or-empty-Neutral n)
  or-empty-Neutral (fstₙ n)          = fstₙ (or-empty-Neutral n)
  or-empty-Neutral (sndₙ n)          = sndₙ (or-empty-Neutral n)
  or-empty-Neutral (natrecₙ n)       = natrecₙ (or-empty-Neutral n)
  or-empty-Neutral (prodrecₙ n)      = prodrecₙ (or-empty-Neutral n)
  or-empty-Neutral (emptyrecₙ n)     = emptyrecₙ (or-empty-Neutral n)
  or-empty-Neutral (unitrecₙ no-η n) = unitrecₙ no-η
                                         (or-empty-Neutral n)
  or-empty-Neutral (Jₙ n)            = Jₙ (or-empty-Neutral n)
  or-empty-Neutral (Kₙ n)            = Kₙ (or-empty-Neutral n)
  or-empty-Neutral ([]-congₙ n)      = []-congₙ (or-empty-Neutral n)
  or-empty-Neutral (resp ok)         = resp ok
  or-empty-Neutral (set ok)          = set ok
  or-empty-Neutral (qrec n)          = qrec (or-empty-Neutral n)

------------------------------------------------------------------------
-- An alternative representation of neutral terms

-- NeutralAt V ∇ y t means that t is neutral and stuck on the name or
-- variable y.

data NeutralAt {m n} (V : Set a) (∇ : DCon (Term ) m) :
       Nat ⊎ Fin n → Term n → Set a where
  defn      : α ↦⊘∷ A ∈ ∇ → NeutralAt V ∇ (inj₁ α) (defn α)
  var       : V → NeutralAt V ∇ (inj₂ x) (var x)
  supᵘˡₙ    : NeutralAt V ∇ y t → NeutralAt V ∇ y (t supᵘ u)
  supᵘʳₙ    : NeutralAt V ∇ y u → NeutralAt V ∇ y (sucᵘ t supᵘ u)
  lowerₙ    : NeutralAt V ∇ y t → NeutralAt V ∇ y (lower t)
  ∘ₙ        : NeutralAt V ∇ y t → NeutralAt V ∇ y (t ∘⟨ p ⟩ u)
  fstₙ      : NeutralAt V ∇ y t → NeutralAt V ∇ y (fst p t)
  sndₙ      : NeutralAt V ∇ y t → NeutralAt V ∇ y (snd p t)
  natrecₙ   : NeutralAt V ∇ y v → NeutralAt V ∇ y (natrec p q r A t u v)
  prodrecₙ  : NeutralAt V ∇ y t → NeutralAt V ∇ y (prodrec r p q C t u)
  emptyrecₙ : NeutralAt V ∇ y t → NeutralAt V ∇ y (emptyrec p A t)
  unitrecₙ  : ¬ Unitʷ-η →
              NeutralAt V ∇ y t → NeutralAt V ∇ y (unitrec p q A t u)
  Jₙ        : NeutralAt V ∇ y w → NeutralAt V ∇ y (J p q A t B u v w)
  Kₙ        : NeutralAt V ∇ y v → NeutralAt V ∇ y (K p A t B u v)
  []-congₙ  : NeutralAt V ∇ y v → NeutralAt V ∇ y ([]-cong s l A t u v)
  qrec      : NeutralAt V ∇ y w → NeutralAt V ∇ y (qrec C t u v w)

opaque

  -- Terms that are "NeutralAt x" are neutral

  NeutralAt→Neutral : NeutralAt V ∇ y t → Neutral V ∇ t
  NeutralAt→Neutral (defn α↦)      = defn α↦
  NeutralAt→Neutral (var ok)       = var ok _
  NeutralAt→Neutral (supᵘˡₙ n)     = supᵘˡₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (supᵘʳₙ n)     = supᵘʳₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (lowerₙ n)     = lowerₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (∘ₙ n)         = ∘ₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (fstₙ n)       = fstₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (sndₙ n)       = sndₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (natrecₙ n)    = natrecₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (prodrecₙ n)   = prodrecₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (emptyrecₙ n)  = emptyrecₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (unitrecₙ x n) = unitrecₙ x (NeutralAt→Neutral n)
  NeutralAt→Neutral (Jₙ n)         = Jₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (Kₙ n)         = Kₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral ([]-congₙ n)   = []-congₙ (NeutralAt→Neutral n)
  NeutralAt→Neutral (qrec n)       = qrec (NeutralAt→Neutral n)