This entry is about a notion in formal logic (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 formal logic such as type theory a telescope $\Delta$ is a finite list of terms in context, whose elements/terms/inhabitants are substitutions.
In dependent type theory, telescopes are defined inductively with the following rules
The substitutions of telescopes are defined inductively with the following rules
which are mutually defined with their action on terms and types.
Théo Winterhalter?, Formalisation and Meta-Theory of Type Theory (web)
Mike Shulman, Towards a Third-Generation HOTT Part 2 (slides, video)
Last revised on June 4, 2022 at 15:04:06. See the history of this page for a list of all contributions to it.