Telescope

In dependent type theory, a telescope is a sequence of term binders x_1 : A_1, x_2 : A_2(x_1), ..., x_n : A_n(x_1,...,x_{n-1}) 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, n-ary binders, and LF signatures. Telescopes can be seen as a judgmental representation of iterated sigma types.

References

@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}",
}