how did I not notice the relationship between telescopes and neutral spines before?

a telescope is a way of looking at function types. { A : Type } -> A -> Int can be flattened down into e.g. ([{ A : Type }, ( _ : A) ], Int).

the list is basically a context, and each name in it can be used in the types of later entries, as well as in the body.

a neutral spine is a representation for values used in normalization-by-evaluation consisting of a variable at the head, followed by a (snoc) list of eliminations (e.g. values to apply the value the variable represents to).

f a 0 can be flattened down into (f, Nil :> a :> 0)

telescopes are type-y things, spines are term-y things (tho note you can have kind-level telescopes and type-level spines), and they grow at opposite ends; but a telescope can describe the type of a neutral spine.

if f’s type is described as a telescope, then the types of its eliminations (arguments) will be the types in the telescope’s context, and the neutral term as a whole will have the final result type of the telescope.