Telescope

Idea

A telescope is strictly positive in the distinguished sort variable $\dot{Q}$ when every occurrence of $\dot{Q}$ appears only as an output or result type of data supplied to a constructor, never to the left of an unrestricted function arrow.

Definition

Fix a type-theoretic context containing a distinguished sort symbol

$\dot{Q}:\mathcal{U}.$

A telescope over $\dot{Q}$ is a finite dependent context

$\Phi [\dot{Q}]\equiv x_1:A_1[\dot{Q}];x_2:A_2[\dot{Q},x_1];\dots ;x_k:A_k[\dot{Q},x_1,\dots ,x_{k-1}].$

We say that $\Phi [\dot{Q}]$ is strictly positive in $\dot{Q}$ if each type $A_i$ is strictly positive in $\dot{Q}$ in the previous context

$\dot{Q}:\mathcal{U};x_1:A_1;\dots ;x_{i-1}:A_{i-1}.$

So the main definition is the corresponding definition for types.

Strictly positive types

Relative to a context $\Gamma ,\dot{Q}:\mathcal{U}$, define the class of types strictly positive in $\dot{Q}$ inductively as follows.

1. If $A$ does not mention $\dot{Q}$, then $A$ is strictly positive in $\dot{Q}$.
2. The sort $\dot{Q}$ itself is strictly positive in $\dot{Q}$.
3. If $A$ is strictly positive in $\dot{Q}$, and $B$ is strictly positive in $\dot{Q}$ in context $\Gamma ,x:A$, then

${\Sigma }_{x:A}B$

is strictly positive in $\dot{Q}$.

4. If $A$ does not mention $\dot{Q}$, and $B$ is strictly positive in $\dot{Q}$ in context $\Gamma ,x:A$, then

${\Pi }_{x:A}B$

is strictly positive in $\dot{Q}$.

Equivalently, function spaces

$A\to B$

are allowed when $\dot{Q}$ occurs strictly positively in $B$ and does not occur in $A$.

5. If $A$ is strictly positive in $\dot{Q}$, and $s,t:A$ are terms whose occurrences of $\dot{Q}$ are strictly positive, then

$s{=}_{A}t$

is strictly positive in $\dot{Q}$.

Depending on how syntactic the definition is meant to be, clause 5 can be omitted from the definition of point-constructor telescopes and included only for path-constructor telescopes. For QIT signatures, it is often useful to allow identity types in the path-constructor telescope.

Intuition

Allowed examples:

$(x:\dot{Q})$

$(f:\mathbb{N}\to \dot{Q})$

$(xs:\mathbb{N}\to \dot{Q}),(p:xs(0){=}_{\dot{Q}}xs(1))$

$(a:A),(f:B(a)\to \dot{Q})$

provided $A$ and $B(a)$ do not themselves mention $\dot{Q}$.

Not allowed:

$(f:\dot{Q}\to \mathbb{N})$

because $\dot{Q}$ appears to the left of an arrow.

Also not allowed:

$(F:(\dot{Q}\to \dot{Q})\to \dot{Q})$

because the argument type $\dot{Q}\to \dot{Q}$ contains a negative occurrence of $\dot{Q}$.

Summary formulation

Let $\dot{Q}$ be a distinguished sort symbol. A telescope

$\Phi [\dot{Q}]\equiv (x_1:A_1),\dots ,(x_k:A_k)$

is strictly positive in $\dot{Q}$ if each type $A_i$ is generated by the grammar of strictly positive types in $\dot{Q}$. This grammar allows $\dot{Q}$ itself, types not mentioning $\dot{Q}$, dependent sums, identity types, and dependent products ${\Pi }_{x:A}B$ only when the domain $A$ does not mention $\dot{Q}$ and the codomain $B$ is strictly positive in $\dot{Q}$. Equivalently, $\dot{Q}$ may occur as data produced or indexed by the constructor, but never as an argument to an unrestricted function space.

Signature notation

For a path constructor telescope, it is clearer to bind the telescope variable explicitly:

$\psi :{\Psi }_j[\dot{Q}]⊢l_j(\psi ),r_j(\psi ):\dot{Q}.$

Equivalently,

$l_j,r_j:(\psi :{\Psi }_j[\dot{Q}])\to \dot{Q}.$

After interpreting $\dot{Q}$ as the generated type $Q$, the constructor types become

$c_i:(\varphi :{\Phi }_i[Q])\to Q$

and

$p_j:(\psi :{\Psi }_j[Q])\to l_j(\psi ){=}_Q{r}_j(\psi ).$