In dependent type theory, a telescope is a sequence of term binders in which types can depend on previous variables.
Telescopes were introduced by de Bruijn [1991] and feature prominently in the implementation and metatheory of dependent type theory, where they are used to represent, e.g., contexts, -ary binders, and LF signatures. Telescopes can be seen as a judgmental representation of iterated sigma types.
de Bruijn, N. G. 1991. Telescopic mappings in typed lambda calculus. Information and Computation 91(2). https://doi.org/10.1016/0890-5401(91)90066-B.
@article{DEBRUIJN1991189,
title = "Telescopic mappings in typed lambda calculus",
journal = "Information and Computation",
volume = "91",
number = "2",
pages = "189 - 204",
year = "1991",
issn = "0890-5401",
doi = "https://doi.org/10.1016/0890-5401(91)90066-B",
url = "http://www.sciencedirect.com/science/article/pii/089054019190066B",
author = "N.G. {de Bruijn}",
}