This entry is about a notion in dependent type theory. For the notion in homotopy theory see at mapping telescope.
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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
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.
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:
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]
Last revised on May 17, 2024 at 14:56:35. See the history of this page for a list of all contributions to it.