nLab type telescope

This entry is about a notion in formal logic (type theory). For the notion in homotopy theory see at mapping telescope.

---

Idea

In formal logic such as type theory a telescope $\Delta$ is a finite list of terms in context, whose elements/terms/inhabitants are substitutions.

Definition

In dependent type theory, telescopes are defined inductively with the following rules

$$\frac{}{\epsilon\; \mathrm{tel}} \qquad \frac{\Delta\; \mathrm{tel} \quad \Delta \vdash A \mathrm{type}}{(\Delta,x:A)\; \mathrm{tel}}$$

The substitutions of telescopes are defined inductively with the following rules

$$\frac{}{():\epsilon} \qquad \frac{\delta:\Delta \quad \Delta \vdash A \mathrm{type} \quad a:A[\delta]}{(\delta,a):(\Delta,x:A)}$$

which are mutually defined with their action on terms and types.

$$\frac{\Delta \vdash A\; \mathrm{type} \quad \delta:\Delta}{A[\delta]\; \mathrm{type}} \qquad \frac{\Delta \vdash a:A \quad \delta:\Delta}{a[\delta]:A[\delta]}$$

See also

• term in context

• dependent type

• dependent identity type

References

• Théo Winterhalter?, Formalisation and Meta-Theory of Type Theory (web)

• Mike Shulman, Towards a Third-Generation HOTT Part 2 (slides, video)