how did I not notice the relationship between telescopes and neutral spines before?
Conversation
You should also notice that telescopes, contexts (in a DTT), theory presentations, specifications, module signatures, records-as-Sigma-types and traits are also essentially all the same, especially in a dependently typed setting.
2
12
In general, we have uses for a generic idea of defining some valid X (which can be a type or a term or ...) using names in scopes as part of the definition of X. These naturally for a DAG (unless you go for mutual recursion too).
2
2
It is important to note that some of these (contexts, telescopes) have their morphisms (substitution) go in the opposite direction of some others (specifications). So pullbacks are 'natural' in contexts, while pushouts in specifications.
1
1
This is why you see pushouts all over the work of Goguen and Burstall, and everything that follows. Including the spectacular work of Doug Smith (and co-authors) from Kestrel on building specs via colimits. But in categorical logic, it's pullbacks everywhere.
1
1
An important remark (which is key to things working in arxiv.org/abs/1812.08079 when you want to build combinators for these things) is that display maps are much better behaved than "adding new terms", as far as compositionality is concerned.
2
3
Ohh this looks interesting! Do you know if there might be a good solution to manifest fields/singleton types from this perspective? This is something I've been wanting to add to my dependent type system: twitter.com/brendanzab/sta - unclear about the best approach though 😅
Quote Tweet
Trying to avoid having top level commands in my dependently typed language. It's frustrating that you can't give a type to a signature easily! You need manifest fields or singletons or identity type trickery to make certain definitions public, or else you limit expressiveness. 
Show this thread
What you show in that thread ought to work in a dependently typed system. The point is that later types (and terms) are interpreted in the context where the previous instantiations are done. So A = U32 is known (and substituted in), so that len is fine [in your example].
1