what’s a telescope in dependently-typed programming, anyway? it seems to me that people use it without fully understanding them. the closest definition I got was “the dependent equivalent of an arrow”, what’s an arrow in this context?
Conversation
I dunno the category theory business, but IIUC it's a sequence of terms where each term might depend on previous terms. Coined by de Bruijn in:
1
7
It alludes to how each variable scopes over subsequent variables in a nested fashion, like how the segments of an “old-fashioned” expandable telescope slide into each other.