nLab type telescope

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

---

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.

See also

• term in context

• dependent type

• structure, structure identity principle

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$”.

and eventually published by de Bruijn in:

• Nicolaas de Bruijn, Telescopic mappings in typed lambda calculus, Information and Computation 91 2 (1991) 189-204 [doi:10.1016/0890-5401(91)90066-B]

The notion is used in much of the dependent type theoretic literature on formalizing mathematical structures, e.g.:

• Claudio Sacerdoti Coen, Enrico Tassi, p. 2 of: Working with Mathematical Structures in Type Theory, in: Types for Proofs and Programs. TYPES 2007, Lecture Notes in Computer Science 4941 Springer (2008) [doi:10.1007/978-3-540-68103-8_11, pdf]

• François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau, §2.3 in: Packaging Mathematical Structures, in: Theorem Proving in Higher Order Logics. TPHOLs 2009, Lecture Notes in Computer Science 5674, Springer (2009) [doi:10.1007/978-3-642-03359-9_23]

and more widely, often without attribution, for instance in:

• Théo Winterhalter, p. 100, 111 in: Formalisation and Meta-Theory of Type Theory, Nantes (2020) [pdf, github]

• Mike Shulman, p. 5-6 in Towards a Third-Generation HOTT Part 2 (2022) [slides pdf, video]

• Astra Kolomatskaia, Michael Shulman, p. 16-18 in Displayed Type Theory and Semi-Simplicial Types [arXiv:2311.18781]