# nLab type telescope

Contents

This entry is about a notion in dependent type theory. For the notion in homotopy theory see at mapping telescope.

# Contents

## Idea

In dependent type theory, by a telescope type or just telescope (terminology due to de Bruijn‘s work on Automath in the early 1970s) one means [Zucker (1975, §10.2), de Bruijn (1991)] an iterated dependent pair-type, hence (in the notation here) a type of the form

$\Gamma \;\;\;\;\;\; \vdash \;\;\;\;\;\; \big( d_1 \colon D_1 \big) \times \big( d_2 \colon D_2(d_1) \big) \times \big( d_3 \colon D_3(d_1, d_2) \big) \times \cdots \times \big( d_{n+1} \colon D_{n+1}(d_1, \cdots , d_{n}) \big) \;\;\; \colon \;\;\; Type \,.$

The notion was motivated by and still plays a key role in the formalization of data structures/mathematical structures in dependently typed proof assistants, which typically appear as such telescope types (also: “record types”, “type classes”, cf. Coen & Tassi (2008, p. 2), Garillot, Gonthier, Mahboubi & Rideau (2009, §2.3)) starting with an underlying data base type and successively adding access functions and then consistency certificates: see the examples listed there.

## References

The notion of telescope types in the sense of iterated dependent pairs goes back to Nicolaas de Bruijn‘s axiomatization of mathematical structures via the Automath proof assistant in the early 1970s, as such referenced in:

• Jeffery Zucker, §10.2 of Formalization of Classical Mathematics in Automath, Colloques Internationaux du Centre National de la Recherche Scientifique 249 (1975) 135-145 [web, pdf]

also in: Studies in Logic and the Foundations of Mathematics 133 (1994) 127-139 [doi:10.1016/S0049-237X(08)70202-7]

[Zucker (1975, §10.2):] Now a general framework in which to view linear orders, or other algebraic structures, has been proposed by de Bruijn. It uses the notion of “telescope”. […] A telescope therefore functions like a “generalized $\sum$”.