nLab type telescope

Contents

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


Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

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

Γ(d 1:D 1)×(d 2:D 2(d 1))×(d 3:D 3(d 1,d 2))××(d n+1:D n+1(d 1,,d n)):Type. \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

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:

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:

Last revised on January 12, 2024 at 17:09:29. See the history of this page for a list of all contributions to it.