We introduce Displayed Type Theory (dTT), a multi-modal homotopy type
theory with discrete and simplicial modes. In the intended
semantics, the discrete mode is interpreted by a model for an arbitrary
$\infty$-topos, while the simplicial mode is interpreted by Reedy fibrant
augmented semi-simplicial diagrams in that model. This simplicial structure is
represented inside the theory by a primitive notion of display or
dependency, guarded by modalities, yielding a partially-internal form of
unary parametricity.

Using the display primitive, we then give a coinductive definition, at
the simplicial mode, of a type $\SST$ of semi-simplicial
types. Roughly speaking, a semi-simplicial type $X$ consists of a type
$X_0$ together with, for each $x:X_0$, a displayed semi-simplicial
type over $X$.  This mimics how simplices can be generated
geometrically through repeated cones, and is made possible by the
display primitive at the simplicial mode. The discrete part of $\SST$
then yields the usual infinite indexed definition of semi-simplicial
types, both semantically and syntactically. Thus, dTT enables working
with semi-simplicial types in full semantic generality.

§ INTRODUCTION

Semi-simplicial types.

Homotopy Type Theory [28] is a perspective on intensional dependent type theory that regards types as homotopical spaces or $\infty$-groupoids.
It has proven remarkably successful as a synthetic context in which to do homotopy theory and algebraic topology, and as an internal language for $(\infty,1)$-toposes [26].
However, an enduring frustration has been its apparent inability to define general homotopy-coherent structures.
Some infinite structures can be defined in HoTT, such as globular types and spectra; but others, such as $A_\infty$-spaces or $(\infty,1)$-categories, have so far resisted all attempts at definition.
We know no convincing explanation for why they should be impossible, but the fact that all attempts appear to fail in a similar way suggests the operation of an as-yet-unarticulated principle.

Specifically, stating an `infinite coherence' property generally seems to require an infinite structure within which to assemble the coherences, while defining such a structure itself seems to require infinite coherence, leading to an infinite regress.
This is in contrast to the situation in classical homotopy theory where the infinite structures to describe coherence, such as operads and simplicial diagrams, can themselves be defined using strict point-set-level equalities, which are then automatically fully coherent.
It is tempting to try to mimic this in homotopy type theory using definitional equalities in place of point-set ones, but this is difficult because definitional equality is not reified in the theory and we have limited tools for forcing it to hold.

One of the more flexible ways to enforce definitional equalities is to use type dependency, moving from a fibred perspective to an indexed one.
In the simplest case, this means replacing a function $\p : \E \to \B$ with a type family $\cblu{\widetilde{E}} : \B \to \Type$.
This has a corresponding projection function $\pi_\cred{1} : \Sigma~\cblu{\widetilde{E}} \to \B$, but we can suppose a point $\cblu{\widetilde{e}} : \Sigma~\cblu{\widetilde{E}}$ with a definitional equality $\pi_\cred{1}~\cblu{\widetilde{e}} \equiv \cblu{b}$ by supposing a point $\cblu{e}: \cblu{\widetilde{E}}~\cblu{b}$ and letting $\cblu{\widetilde{e}} = \bkt{\cblu{b},~\cblu{e}}$.

Thus, it is natural to try to define infinitely coherent structures that can be expressed in a purely indexed way.
The example of this sort which has attracted the most attention is that of semi-simplicial types, because they are well-known within homotopy theory and could be used to encode many, if not all, other infinitely coherent structures.
In indexed style, a semi-simplicial type consists of type families $\cred{A_0}$, $\cred{A_1}$, $\cred{A_2}$, and so on, having types that start out as follows:

\begin{align*}
\cred{A_0} :~&\mathsf{Type} \\
\cred{A_1} :~&{\normalcolor (\cblu{x\sub{01}} :
\cred{A_0})}~{\normalcolor (\cblu{x\sub{10}} :
\cred{A_0})} \to \mathsf{Type} \\
\cred{A_2} :~&{\normalcolor (\cblu{x\sub{001}} :
\cred{A_0})}~{\normalcolor (\cblu{x\sub{010}} :
\cred{A_0})}
~{(\cblu{\beta\sub{011}} : \cred{A_1}~\cblu{x\sub{001}~x\sub{010}})}
~{\normalcolor (\cblu{x\sub{100}} : \cred{A_0})}
~{(\cblu{\beta\sub{101}} : \cred{A_1}~\cblu{x\sub{001}~x\sub{100}})}
~{(\cblu{\beta\sub{110}} : \cred{A_1}~\cblu{x\sub{010}~x\sub{100}})} \to
\mathsf{Type} \\
\cred{A_3} :~&{\normalcolor (\cblu{x\sub{0001}} :
\cred{A_0})}~{\normalcolor (\cblu{x\sub{0010}} :
\cred{A_0})}
~{(\cblu{\beta\sub{0011}} : \cred{A_1}~\cblu{x\sub{0001}~x\sub{0010}})}
~{\normalcolor (\cblu{x\sub{0100}} : \cred{A_0})}
~{(\cblu{\beta\sub{0101}} : \cred{A_1}~\cblu{x\sub{0001}~x\sub{0100}})}
~{(\cblu{\beta\sub{0110}} : \cred{A_1}~\cblu{x\sub{0010}~x\sub{0100}})} \\
&{(\cblu{\ff\sub{0111}} :
\cred{A_2}~\cblu{x\sub{0001}~x\sub{0010}~\beta\sub{0011}~x\sub{0100}~\beta\sub{0101}~\beta\sub{0110}})}
~{\normalcolor (\cblu{x\sub{1000}} : \cred{A_0})}
~{(\cblu{\beta\sub{1001}} : \cred{A_1}~\cblu{x\sub{0001}~x\sub{1000}})}
~{(\cblu{\beta\sub{1010}} : \cred{A_1}~\cblu{x\sub{0010}~x\sub{1000}})}\\
&{(\cblu{\ff\sub{1011}} :
\cred{A_2}~\cblu{x\sub{0001}~x\sub{0010}~\beta\sub{0011}~x\sub{1000}~\beta\sub{1001}~\beta\sub{1010}})}
~{(\cblu{\beta\sub{1100}} : \cred{A_1}~\cblu{x\sub{0100}~x\sub{1000}})}
~{(\cblu{\ff\sub{1101}} :
\cred{A_2}~\cblu{x\sub{0001}~x\sub{0100}~\beta\sub{0101}~x\sub{1000}~\beta\sub{1001}~\beta\sub{1100}})}\\
&{(\cblu{\ff\sub{1110}} :
\cred{A_2}~\cblu{x\sub{0010}~x\sub{0100}~\beta\sub{0110}~x\sub{1000}~\beta\sub{1010}~\beta\sub{1100}})} \to
\mathsf{Type}
\end{align*}

First, we have a type $\cred{A_0}$ of points. Second, we
have for every two points $\cblu{x\sub{01}},\cblu{x\sub{10}} : \cred{A_0}$, a type
$\cred{A_1}~\cblu{x\sub{01}~x\sub{10}}$ of lines joining $\cblu{x\sub{01}}$ and $\cblu{x\sub{10}}$.
Third, for every three points $\cblu{x\sub{001}},\cblu{x\sub{010}},\cblu{x\sub{100}} : \cred{A_0}$ and
three lines $\cblu{\beta\sub{011}} : \cred{A_0}~\cblu{x\sub{001}~x\sub{010}}$, $\cblu{\beta\sub{101}} :
\cred{A_0}~\cblu{x\sub{001}~x\sub{100}}$, and $\cblu{\beta\sub{110}} : \cred{A_0}~\cblu{x\sub{010}~x\sub{100}}$, a type
$\cred{A_1}~\cblu{x\sub{001}~x\sub{010}~\beta\sub{011}~x\sub{100}~\beta\sub{101}~\beta\sub{110}}$ of triangles with the given
boundary. The pattern continues with tetrahedra, which we may also, more
technically, call $\cred{3}$-simplices. In general, $\cred{A}_\n$ describes the type of
$\n$-simplices indexed by their boundaries.

The binary subscripts on variables above following a scheme proposed by Tim Campion.
In this scheme, the $\cred{2}^{\n+\cred{1}}-\cred{1}$ simplices constituting an $\n$-simplex and its boundary are labeled by the numbers from $\cred{1}$ to $\cred{2}^{\n+\cred{1}}-\cred{1}$ written in binary, where the number of $\cred{1}$s in a binary number corresponds to the dimension of the simplex, and the binary numbers corresponding to the boundary of some simplex are obtained by replacing one or more of the $\cred{1}$s in its binary number by $\cred{0}$s.
(As we will see later, the binary number $\cred{0}$ can also be regarded as denoting the unique $(\minusone)$-simplex in the boundary of an $\n$-simplex in an augmented semi-simplicial set.)

We then list these simplices in the order given by these numbers.
This ordering may seem somewhat curious, compared to the more naïve approach of listing all the $\cred{0}$-simplices, then all the $\cred{1}$-simplices, and so on; but it does retain the important property that all the simplices in the boundary of some simplex are listed before it (thus, for instance, it makes the semi-simplex category into an `ordered inverse category' in the sense of <cit.>).
We will see later that this ordering is what arises most naturally in (co)inductive constructions of semi-simplicial sets (which was also Campion's motivation).

In addition to subscripting simplex variables by binary numbers according to this scheme, in this paper we will use different base letters to indicate the dimension of each variable.
Thus for instance $\cblu{x\sub{001}}$, $\cblu{x\sub{010}}$, and $\cblu{x\sub{100}}$ are all $\cred{0}$-simplices, while $\cblu{\beta\sub{011}}$, $\cblu{\beta\sub{101}}$, and $\cblu{\beta\sub{110}}$ are all $\cred{1}$-simplices, and $\cblu{\ff\sub{111}}$ is a $\cred{2}$-simplex.
We will not have much occasion to denote $\cred{3}$-simplices; for $(\minusone)$-simplices we use the Cyrillic letter $\ze$.
We may also use different letters from the same alphabets for simplices in different semi-simplicial types, e.g. $\cblu{\gamma\sub{11}} : \cred{B_1}~\cblu{y\sub{01}}~\cblu{y\sub{10}}$ and $\cblu{\delta\sub{11}} : \cred{C_1}~\cblu{z\sub{01}}~\cblu{z\sub{10}}$.

One may think of the terms $\cred{A_0}$, $\cred{A_1}$, $\cred{A_2}$, and so on as defining the fields of an infinite record type.
Terms of this infinite record type $\SST$ are known as semi-simplicial types.
Thus, the problem is to define a type of semi-simplicial types within homotopy type theory, continuing the above pattern.
As a correctness criterion, one would expect that when interpreted in any $(\infty,1)$-topos the type $\SST$ becomes a classifier of semi-simplicial objects.
However, even this problem is still unsolved: every attempt to internally encode the combinatorics that generate the type of $\cred{A}_\n$, as a function of $\n$, seems to lead once again to an infinite regress.

In light of this situation, an alternative approach is to formulate more expressive type theories that can solve the problem of infinitely coherent objects.
One such proposal is Two-Level Type Theory (2LTT) [1], which introduces an `outer level' of `exo-types' that are not homotopy-invariant.
The exo-types admit a strict exo-equality type, essentially reifying definitional equality, which can then be used analogously to classical point-set equality to define infinitely coherent structures.
And by the results of [29], 2LTT can be interpreted in any $(\infty,1)$-topos, so its semantics are not significantly less general than ordinary HoTT, and the type $\SST$ defined in 2LTT does interpret to the correct classifier.
However, although the exo-equality is assumed to satisfy Uniqueness of Identity Proofs, to keep type-checking decidable it cannot satisfy a reflection rule making exo-equalities into definitional equalities.
Thus, it can be quite cumbersome to work with in practice.

Another proposal is Simplicial Type Theory (STT) [23], which changes perspective to view individual types as simplicial spaces, with additional primitives for manipulating the simplicial structure.
One can then simply impose conditions on one of these `simplicial types' to make it represent (for instance) an $(\infty,1)$-category.
This suggests a `synthetic' approach to higher category theory analogous to ordinary HoTT's synthetic approach to homotopy theory, which is potentially quite powerful; and the results of [23, 31] imply that it can be interpreted in the category of simplicial objects in any $(\infty,1)$-topos.
However, the strength of the synthetic approach is also its weakness: because simplicial types are postulated rather than defined, what we can do with them is limited to what is expressed by the axiomatization.

A coinductive definition of semi-simplicial types.

In this paper we propose a third enhancement of homotopy type theory, called Displayed Type Theory (dTT), in which it is possible to define and work with semi-simplicial types (and many other things).
This type theory is inspired by the following idea for a coinductive definition of a type $\SST$ of semi-simplicial types:

A semi-simplicial type $\A$ consists of

* a type $\Z~\A$, and

* for each $\x : \Z~\A$, a semi-simplicial type $\S~\A~\x$ over $\A$.

It may not be at all obvious why this should be a definition of semi-simplicial types, so let us unravel it a few steps:

* Every semi-simplicial type $\A$ has a type $\Z~\A$, whose points we call $\cred{0}$-simplices of $\A$.
Thus we may also write $\A_\cblu{0} = \Z~\A$.

* Every $\cred{0}$-simplex $\x : \A_\cblu{0}$ gives rise to a semi-simplicial type $\S~\A~\x$ over $\A$, called the slice of $\A$ over $\x$.
Of course, if we don't know what a semi-simplicial type is, we can't be expected to know what one semi-simplicial type over another one is — at least, not completely.
But we do know that every semi-simplicial type $\A$ has an underlying type $\Z~\A$, so it stands to reason that a semi-simplicial type $\B$ over $\A$ should in particular have an underlying type $\Z\d~\B$ over $\Z~\A$, i.e. a type family $\Z\d~\B: \Z~\A \to \Type$.
Thus, in particular for every $\x : \A_\cblu{0}$ we have $\Z\d~(\S~\A~\x) : \A_\cblu{0} \to \Type$, hence for every additional $\y: \A_\cblu{0}$ we have a type $\Z\d~(\S~\A~\x)~\y$.
We call this the type $\A_\cblu{1}~\x~\y$ of $\cred{1}$-simplices from $\x$ to $\y$.

* Now we know that every semi-simplicial type $\A$ has not only an underlying type of $\cred{0}$-simplices $\A_\cblu{0}$, but for every $\cblu{x\sub{01}},\cblu{x\sub{10}} : \A_\cblu{0}$ a type $\A_\cblu{1}~\cblu{x\sub{01}}~\cblu{x\sub{10}}$ of $\cred{1}$-simplices.
Therefore, it stands to reason that any semi-simplicial type $\B$ over $\A$ should also have, not only a type family $\B_\cblu{0}$ over $\A_\cblu{0}$, but a type family $\B_\cblu{1}$ over $\A_\cblu{1}$.
Thinking of $\A_\cblu{1}$ as an indexed representation of a span $\A_\cblu{0} \leftarrow \int~\A_\cblu{1} \to \A_\cblu{0}$, we deduce that $\B_\cblu{1}$ should be an indexed representation of a span morphism

\[
\begin{tikzcd}
\int~\B_\cblu{0} \ar[d] & \int\int~\B_\cblu{1} \ar[l] \ar[r] \ar[d] & \int~\B_\cblu{0} \ar[d] \\
\A_\cblu{0} & \int~\A_\cblu{1} \ar[l] \ar[r] & \A_\cblu{0}
\end{tikzcd}
\]

and therefore we should have

\[\B_\cblu{1} : (\cblu{y\sub{01}} : \A_{\cblu{0}})~(\cblu{z\sub{01}} : \B_{\cblu{0}}~\cblu{y\sub{01}})~(\cblu{y\sub{10}} : \A_{\cblu{0}})~(\cblu{z\sub{10}} : \B_{\cblu{0}}~\cblu{y\sub{10}})~(\cblu{\gamma\sub{11}} : \A_{\cblu{1}}~\cblu{y\sub{01}}~\cblu{y\sub{10}}) \to \Type.\]

More precisely, since every $\cred{0}$-simplex $\cblu{y\sub{01}}$ of $\A$ gives rise to a semi-simplicial type $\S~\A~\cblu{y\sub{01}}$ over $\A$, any $\cred{0}$-simplex $\cblu{z\sub{01}}$ of $\B$ over $\cblu{y\sub{01}}$ should give rise to a semi-simplicial type $\S\d~\B~\cblu{y\sub{01}}~\cblu{z\sub{01}}$ over both $\B$ and $\S~\A~\cblu{y\sub{01}}$.
But the common dependence on $\A$ should be shared, so $\S\d~\B~\cblu{y\sub{01}}~\cblu{z\sub{01}}$ should live over the cospan $\B \rightarrow \A \leftarrow \S~\A~\cblu{y\sub{01}}$:

\[
\begin{tikzcd}
\B \ar[d] & \S\d~\B~\cblu{y\sub{01}}~\cblu{z\sub{01}} \ar[l] \ar[d] \\
\A & \S~\A~\cblu{y\sub{01}} \ar[l]
\end{tikzcd}
\]

Passing to $\cred{0}$-simplices, this means that $\Z\d\d\bkt{\S\d~\B~\cblu{y\sub{01}}~\cblu{z\sub{01}}}$ should be a type dependent on $\cblu{y\sub{10}}:\A_{\cblu{0}}$, $\cblu{z\sub{10}} : \B_{\cblu{0}}~\cblu{y\sub{10}}$, and $\cblu{y_{11}}:(\S~\A~\cblu{y\sub{01}})_0~\cblu{y\sub{10}} \equiv \A_{\cblu{1}}~\cblu{y\sub{01}}~\cblu{y\sub{10}}$.
Thus we can define the 1-simplices of $\B$ as $\B_{\cblu{1}}~\cblu{y\sub{01}}~\cblu{z\sub{01}}~\cblu{y\sub{10}}~\cblu{z\sub{10}}~\cblu{\gamma\sub{11}} \equiv \Z\d\d\bkt{\S\d~\B~\cblu{y\sub{01}}~\cblu{z\sub{01}}}~\cblu{y\sub{10}}~\cblu{z\sub{10}}~\cblu{\gamma\sub{11}}$.

In particular, therefore, since for any $\x : \A_\cblu{0}$ we have a semi-simplicial type $\S~\A~\x$ over $\A$, we have

\[ \bkt{\S~\A~\x}_\cblu{1} : (\cblu{y\sub{01}} : \A_\cblu{0})~(\cblu{z\sub{01}} : \bkt{\S~\A~\x}_\cblu{0}~\cblu{y\sub{01}})~(\cblu{y\sub{10}} : \A_\cblu{0})~(\cblu{\cblu{z\sub{10}}} : \bkt{\S~\A~\x}_\cblu{0}~\cblu{y\sub{10}})~(\cblu{\cblu{\gamma\sub{11}}} : \A_\cblu{1}~\cblu{y\sub{01}}~\cblu{y\sub{10}}) \to \Type. \]

Since $\bkt{\S~\A~\x}_\cblu{0}~\cblu{y\sub{01}} \equiv \A_\cblu{1}~\x~\cblu{y\sub{01}}$ by definition, this is equivalently

\[ \bkt{\S~\A~\x}_\cblu{1} : (\cblu{y\sub{01}}:\A_\cblu{0})~(\cblu{z\sub{01}} : \A_\cblu{1}~\x~\cblu{y\sub{01}})~(\cblu{y\sub{10}}:\A_\cblu{0})~(\cblu{\cblu{z\sub{10}}} : \A_\cblu{1}~\x~\cblu{y\sub{10}})~(\cblu{\cblu{\gamma\sub{11}}} : \A_\cblu{1}~\cblu{y\sub{01}}~\cblu{y\sub{10}}) \to \Type. \]

Renaming the variables as $\cblu{y\sub{ab}}\equiv \cblu{x\sub{ab0}}$, $\cblu{\gamma\sub{ab}}\equiv \cblu{\beta\sub{ab0}}$, and $\cblu{z\sub{ab}}\equiv \cblu{\beta\sub{ab1}}$, and writing $\x\equiv \cblu{x\sub{001}}$, this becomes

\[ \bkt{\S~\A~\cblu{x\sub{001}}}_\cblu{1} : (\cblu{x\sub{010}}:\A_\cblu{0})~(\cblu{\beta\sub{011}} : \A_\cblu{1}~\cblu{x\sub{001}}~\cblu{x\sub{010}})~(\cblu{x\sub{100}}:\A_\cblu{0})~(\cblu{\cblu{\beta\sub{101}}} : \A_\cblu{1}~\cblu{x\sub{001}}~\cblu{x\sub{100}})~(\cblu{\cblu{\beta\sub{110}}} : \A_\cblu{1}~\cblu{x\sub{010}}~\cblu{x\sub{100}}) \to \Type. \]

Thus, this is precisely correct to be a type of $\cred{2}$-simplices:

\[ \A_\cblu{2}~\cblu{x\sub{001}}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}}~\cblu{x\sub{100}}~\cblu{\cblu{\beta\sub{101}}}~\cblu{\cblu{\beta\sub{110}}} \equiv \bkt{\S~\A~\cblu{x\sub{001}}}_\cblu{1}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}}~\cblu{x\sub{100}}~\cblu{\cblu{\beta\sub{101}}}~\cblu{\cblu{\beta\sub{110}}}. \]

This pattern may be visualised as follows:

(0,-0.2) node[anchor=south]$\Z~\A$;
[color=darkgreen] (0,-1) circle (1.5pt);
(0,-1) node[anchor=south]$\cblu{x\sub{1}}$;
(2,-0.282) node[anchor=south]$\Z\d~\bkt{\S~\A~\cblu{x\sub{01}}}~\cblu{x\sub{10}}$;
[color=darkgreen, thick] (2,-1)–(2,-2.5);
[color=red] (2,-1) circle (1.5pt);
(2,-1) node[anchor=south]$\cprime{x\sub{01}}$;
[color=darkgreen] (2,-2.5) circle (1.5pt);
(2,-2.5) node[anchor=north]$\cblu{x\sub{10}}$;
(2,-1.75) node[anchor=east]$\cblu{x\sub{11}}$;
(6.2,-0.307) node[anchor=south]$\Z\d\d~\bkt{\S\d~\bkt{\S~\A~\cblu{x\sub{001}}}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}}}~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}$;
[color=darkgreen, thick] (5,-1)–(6.3,-1.75);
[color=darkgreen, thick] (5,-2.5)–(6.3,-1.75);
[color=darkgreen] (6.3,-1.75) circle (1.5pt);
[pattern=north west lines, pattern color=darkgreen] (5,-1)–(6.3,-1.75)–(5,-2.5);
[color=red, thick] (5,-1)–(5,-2.5);
[color=red] (5,-1) circle (1.5pt);
(5,-1) node[anchor=south]$\cprime{x\sub{001}}$;
[color=red] (5,-2.5) circle (1.5pt);
(5,-2.5) node[anchor=north]$\cprime{x\sub{010}}$;
(5,-1.75) node[anchor=east]$\cprime{\beta\sub{011}}$;
(6.3,-1.75) node[anchor=west]$\cblu{x\sub{100}}$;
(5.5,-1.75) node$\cblu{\ff\sub{111}}$;
(5.6,-1.45) node[anchor=south west]$\cblu{\beta\sub{101}}$;
(5.6,-2.05) node[anchor=north west]$\cblu{\beta\sub{110}}$;

An alternative, and more geometrical, viewpoint, is that the $\n$-simplex is the cone of the $(\n-\cred{1})$-simplex.
Thus, if we already know that every semi-simplicial type has a suitably indexed type of $(\n-\cred{1})$-simplices, we can conclude the same about the $n$-simplices as follows.
For every $\cred{0}$-simplex $\x$, the dependent semi-simplicial type $\S~\A~\x$ has a type of `dependent $(\n-\cred{1})$-simplices' indexed by the type of $(\n-\cred{1})$-simplices of $\A$.
Thus, an element of this type depends on $\x$ (the cone vertex) as well as an $(\n-\cred{1})$-simplex of $\A$ (the base face, opposite the cone vertex), and its boundary consisting of dependent $\k$-simplices for $<̨-1$ that form cones over all the faces of the base $(-1)$-simplex sharing the same vertex $$.
Together, these form the boundary of an $$-simplex.
(In the ordering of variables induced by the above presentation, the simplices in the base face are interspersed with their dependent versions: thus in the case $≡2$ the faces $x010,x100,β110$ form the base $1$-simplex with $β011,β101$ the dependent $0$-simplices (i.e. $1$-simplices) forming a cone over the boundary $x010,x100$.)
Hopefully this is sufficiently convincing for now; later we will give a precise justification.

As simple and appealing as this \emph{`definition'} is, it is not meaningful in ordinary dependent type theory.
The intuitive claim is that it defines a type $$ by coinduction, with $$ and $$ as destructors.
For $$ this is unproblematic (it is not even corecursive).
However, the output of $$ is not an element of the type $$ being defined, as would be usual for a corecursive destructor of a coinductive type, but a \emph{`dependent element'}, or \emph{`displayed element'}, of $$ over the input of $$.
If we write $$̣ for this putative family of `displayed elements', the types of $\Z$ and $\S$ are

\begin{equation}
\label{eq:ZS-intro}
\begin{aligned}
\Z &: \SST \to \Type \\
\S &: \bkt{\X :\SST} \to \Z~\X \to \SST\d~\X.
\end{aligned}
\end{equation}

We would like to regard this as a sort of `higher coinductive type'.
Just as a higher inductive type can have constructors involving not just elements of the type being defined but also paths therein, here we have a putative coinductive type whose destructors involve not just elements of the type being defined but also `displayed elements' thereof.
Thus, to make sense of this we need a type theory with a primitive operation $\pblank\d$ associating to a type its family of \emph{`displayed elements'}.
As it turns out, the precise notion of $$̣ that we require is a variant of unary internal parametricity.

External and internal parametricity.

In general, by `parametricity' we mean a statement that every type (perhaps subject to contextual restrictions; see below) is equipped with a relation (of some arity), and every function (subject to the same restrictions) preserves those relations.
The original form of parametricity, such as in [30], is a meta-theoretic statement about type theory, in which the relations are meta-theoretic, and the contextual restriction is that it applies only to closed types and terms (those defined in the empty context).
That is, in this `external' parametricity, every closed type is given a relation on its closed terms, which is preserved by every closed function.
For instance, in the unary case, given a closed function $\ec \vdash \f : \A \to \B$, if the $\A$-relation holds of a closed term $\ec\vdash \a:\A$, then the $\B$-relation holds of the closed term $\ec\vdash \f~\a:\B$.
Indeed, the fact that $f$ satisfies this condition is exactly the statement that the $(\A\to\B)$-relation holds of it, and is thus a special case of the `fundamental theorem of logical relations' that every closed term satisfies the relation on its type.
Semantically, external parametricity is obtained by interpreting type theory in a `gluing' or `relational' model.

By contrast, in type theories with fully internal parametricity such as [9, 8, 21], there is no contextual restriction, and the relations are internal (i.e. type families).
In the unary case, this means for any type in any context, say $\Gamma \vdash \A \type$, there is a type family that we will denote $\Gamma,~\x:\A \vdash \A\d~\x \type$, and every function $\Gamma \vdash \f : \A \to \B$ in any context lifts to a function $\Gamma \vdash \f\d : (\x:\A)(\x\cblu{'}:\A\d~\x) \to \B\d~(\f~\x)$ between these type families.
As in the external case, there is a formula for the relation of a function-type:

\begin{equation}
\label{eq:d-pi-intro}
\bkt{\bkt{\a : \A} \to \B~\sqbkt{\a}}\d~\f \equiv \bkt{\a : \A} \bkt{\a\cblu{'} : \A\d~\a} \to \B\d~\sqbkt{\a~, \a\cblu{'}}~\bkt{\f~\a}
\end{equation}

which says that so-called `computability witnesses' for $\f$ take computability witnesses of $\a$ to computability witnesses of $\f~\a$.
Thus the statement that $\f$ preserves computability witnesses is equivalent to saying it lifts to an element $\f\d$ of this type, and is a special case of a general rule that \emph{every} term $Γ⊢:$ lifts to a computability witness $Γ⊢:̣ $.\footnote{The punning of notation is intentional, and indeed consistent, as we will see: the type $\pblank\d$ coincides with the term $\pblank\d$ applied to elements of the universe.}

Such an internalization of parametricity introduces the new possibility of \emph{iterating} it, leading to $̣̣$, $̣̣$̣, and so on.
Semantically, this means that each type must be interpreted by a cubical type (or set), where the arity of the relations determines the number of `boundary points' on each side of the cubes, and the dependencies of each iterated relation on the previous ones supplies the faces of a cube.
Our primary interest is in unary parametricity, where $\A\d$ depends only on one copy of $$; in this case the semantics involves \emph{`unary cubes'} where each edge has only one vertex.\footnote{Geometrically, these can be thought of as powers of a half-open interval $[0,1)^n$, or closed octants $[0,\infty)^n$ in $n$-dimensional Euclidean space.}

The rule lifting any $$ to $$̣ then implies that these cubical types must have degeneracies, taking any cube to a higher-dimensional one with some boundaries trivial.
More surprisingly, it seems that to have good computational behavior and semantic models, the cubical types must also include symmetries (transpositions): from $\cblu{d} \equiv \cred{\lambda}~\x.~\x\d : \bkt{\x : \X} \to \X\d~\x$, we can either directly obtain the type of $\cblu{d}\d$ as $:  ' :  →̣̣  ' $̣ or first perform the computation $\cblu{d}\d \equiv \cblu{\lambda} ~\x~\x\cblu{'}.~\x\cblu{'}\d$ and obtain its type as $:  ' :  →̣̣  '$, and it these must be related by a symmetry operation.

The general advantages of internal parametricity over external are clear: we can reason about computability witnesses while staying within a single type theory, using a single proof assistant.
Moreover, internal parametricity allows us to at least try to make sense of a type $$ with the destructors~\eqref{eq:ZS-intro}.
However, fully internal parametricity is not conservative over ordinary type theory: it is highly nonclassical, incompatible with axioms such as the law of excluded middle; and its semantics is not as general as we would like.
We would like our type theory to be interpretable in any $(∞,1)$-topos (generalizing~[26]), in such a way that our type $$ is interpreted by a category-theoretic \emph{`classifier'} of semi-simplicial objects; but as we have just observed, the semantics of internal parametricity seems to live only in a category of cubical objects.
Now the category of cubical objects in an $(∞,1)$-topos is again an $(∞,1)$-topos, so (using~[26]) we can expect to interpret an internally parametric type theory in the latter; but the connection of this interpretation to the \emph{original} $(∞,1)$-topos is not clear.

\paragraph{Displayed type theory.}

Our solution is to use a \emph{less internally} parametric type theory.
We can think of internal parametricity as arising in three stages.
The first stage is an \emph{external} parametricity model, where types are interpreted by pairs $A_0:,  A_1 :A_0 →$.
In this case $$̣ maps one model to a different model, interpreting an ordinary type by a pair of types; this yields parametricity results as metatheorems.
In the second stage, to make $\A\d$ live in the same model as $$, we iterate this construction infinitely many times; now types are interpreted by \emph{semi-cubical types}, with faces but not degeneracies.
Finally, in the third stage we add a \emph{`degeneracy'} operation $: →$ making every \emph{term} parametric.
This allows proving parametricity theorems \emph{inside} the type theory, and semantically moves us from semi-cubical types to cubical ones.

The solution to our problem is to stop after the \emph{second} stage.
This is advantageous semantically because semi-cubical sets are presheaves on a \emph{direct} category (i.e.\ covariant diagrams on an \emph{inverse} category), and in this case the model construction is much more concrete.
Specifically, in [24] it was shown that from any model of univalent dependent type theory inside of a type theoretic fibration category, one may form a derived model of Reedy fibrant presheaves on any direct category, with the type formers in the presheaf model constructed inductively in terms of those in the original model.
In particular, in degree $0$ all the type-formers act exactly as they do in the original model.
Thus, semantically we can be sure that all our constructions, including $$, specialise to something meaningful in an arbitrary $(∞,1)$-topos.

dTT is a syntax corresponding to this model, which is likewise intermediate between external parametricity and fully internal parametricity: its parametricity primitive $$̣ has a contextual restriction that is weaker than the `only closed terms' requirement of external parametricity, but stronger than the `any context goes' laxity of internal parametricity.
We start by observing that in either cubical or semi-cubical sets, the semantically fundamental parametricity operation actually changes the context: given $\cblu{\Gamma} \vdash \t : \A$, one has $\cblu{\Gamma}\D \vdash \t\d : \A\d~\t$, where $\cblu{\Gamma}\D$ augments $\Gamma$ by computability witnesses of all its variables.
For cubical sets with degeneracies, we can deduce a version of $\pblank\d$ that doesn't change the context by substituting along a degeneracy map $Γ→Γ$ (e.g.\ this is the isomorphism between the \emph{`global'} and \emph{`local'} models of~[2]).
But for semi-cubical sets this is impossible, so we have to bite the bullet and deal with context-modifying operations.

The notion of a non-binding operation that changes contexts is familiar from the realm of modal logic, where, to first approximation, a proof of necessity of some proposition, i.e. of $ $, may only use necessary assumptions.
Modalities in dependent type theory have previously been used to internalise meta-theoretic operations that don't make sense in arbitrary contexts, such as the right adjoint to a $Π$-type in~[20], and we use them similarly here.
Specifically, in dTT we have a modality $$ that partially internalises the notion of \emph{`closed term'} appearing in external parametricity, and which restricts the domain of $$̣.
Thus the only analogue of the above $\cblu{d} \equiv \cred{\lambda}~\x.~\x\d : \bkt{\x : \X} \to \X\d~\x$ in dTT is $\cblu{\widetilde{d}} \equiv \cred{\lambda}~\x.~\x\d : \bkt{\x :^\trisq \X} \to \X\d~\x$.
In particular, modal variables are protected from alteration by $\pblank\d$, so that we have $d≡̣λ . ̣̣: :^ →̣̣  $̣, thereby avoiding the need for symmetry.

In fact, to emphasise further that dTT retains general semantics over an arbitrary $(\infty,1)$-topos, we will use a multimodal type theory [15, 14] with two modes, one for the original topos and the other for the topos of semi-cubical sets.
These modes are related by modalities $\tri$ (the constant semi-cubical type), $\dia$ (the $\cred{0}$-cubes of a cubical type), and $\sq$ (the limit of a cubical type), and $\trisq = \tri\circ\sq$ is a composite endo-modality.
Only $\trisq$ is necessary to formulate display, but the other modalities are also useful to have around: in particular, $\dia$ internalises the process of passing from the model in semi-cubical types to the original model in $\MC$.
For instance, $\dia\SST$ is what corresponds semantically to the classifier of semi-simplicial objects in $\MC$.

Furthermore, display itself may be thought of as a modality, albeit one that is indexed over the original type.
Display falls into into the new and yet underdeveloped framework of indexed modalities, such as the path types of cubical type theory (treated modally in [14]) and the identity types of the forthcoming Higher Observational Type Theory (HOTT) [5, 2].
Moreover, analogously to those cases, we could formulate display either as an inert type-former defined by abstraction over an `interval' (like path types in cubical type theory), or as an operation that computes on most other canonical type-formers (like identity types in HOTT).
In this paper we make the latter choice, so that rules like <ref> are actually definitional equalities.
Formulating such rules computationally is actually easier for dTT than for HOTT, due mainly to the lack of symmetry (although there is a tradeoff, since the presence of modalities is an extra complicating factor).

Until now we have been talking about semi-cubical types to make the connection with parametricity clear, but in the unary case there is an intriging coincidence: the unary semi-cube category is isomorphic to the augmented semi-simplex category,[To see this geometrically, note that the $(\n+\cred{1})$-dimensional octant $[\cred{0},\cred{\infty})^{\n+\cred{1}}$ contains a standard face-preserving embedding of the $\n$-simplex, $\cred{\oldDelta}^\n = \{ (\x_\cred{0},\dots,\x_\n) \in [\cred{0},\cred{\infty})^{\n+\cred{1}} \mid \x_\cred{0}+\cdots +\x_\n = \cred{1}\}$, including the augmentation case $\cred{\oldDelta}^\minusone = \cred{\emptyset}$.] with a dimension shift: the $\n$-cube corresponds to the $(\n-\cred{1})$-simplex.
For this reason we refer to the two modes in our theory as the discrete mode $\dm$ and the simplicial mode $\sm$.
Thus, dTT can actually internalise semi-simplicial types in two ways: as the coinductive type $\SST$ mentioned above, and as the universe of types at the simplicial mode.
The latter suggests that dTT could also be used similarly to simplicial type theory, with types at the simplicial mode treated as synthetic (augmented semi-) simplicial types.

(Note that an augmented semi-simplicial type can be viewed as a family of ordinary semi-simplicial sets indexed by the type of $(\minusone)$-simplices.
Thus, our observation that augmented semi-simplicial types support a better internal language than ordinary ones is analogous to the observation of [22] that parametrised spectra are likewise preferable to unparametrised ones.)

Displayed structures

Our terminology display for the operation $\d$ is inspired by the fact that when applied to record types whose elements are algebraic structures, it produces \emph{displayed structures} of the corresponding sort.
Here a \emph{`displayed structure'} over a structure $$ is a structure $$ of the same kind with a structure map $→$, but reformulated in terms of the corresponding family of fibres $→$.
Working with displayed structures rather than morphisms is a technique for enforcing definitional equalities on images in $$.

The most common displayed structure is a \emph{displayed category}; here the terminology was introduced by~[6].
This arises from the record type of categories, defined in the usual dependently typed way (where we omit the axioms for concision):
\begin{lstlisting}
(*\textbf{record}*) (*$\cred{\mathsf{Cat}}$*) : (*$\Type$*) (*\textbf{where}*)
(*$\cred{\mathsf{ob}}$*) : (*$\Type$*)
(*$\cred{\mathsf{hom}}$*) : (*$\cred{\mathsf{ob}}$*) (*$\to$*) (*$\cred{\mathsf{ob}}$*) (*$\to$*) (*$\Type$*)
(*$\cred{\mathsf{id}}$*) : ((*$\x$*) : (*$\cred{\mathsf{ob}}$*)) (*$\to$*) (*$\cred{\mathsf{hom}}$*) (*$\x$*) (*$\x$*)
(*$\cred{\mathsf{comp}}$*) : {(*$\x$*) (*$\y$*) (*$\z$*) : (*$\cred{\mathsf{ob}}$*)} (*$\to$*) (*$\cred{\mathsf{hom}}$*) (*$\y$*) (*$\z$*) (*$\to$*) (*$\cred{\mathsf{hom}}$*) (*$\x$*) (*$\y$*) (*$\to$*) (*$\cred{\mathsf{hom}}$*) (*$\x$*) (*$\z$*)
\end{lstlisting}
We do not discuss record types (including $Σ$-types) in this paper, but the extension of $$̣ to them produces another record type whose fields have $\d$ applied to them.
For instance, from a $Σ$-type:\\
\begin{minipage}{\textwidth}
\begin{lstlisting}
(*\textbf{record}*) (*$\Sigma$*) ((*$\A$*) : (*$\Type$*)) ((*$\B$*) : (*$\A$*) (*$\to$*) (*$\Type$*)) : (*$\Type$*) (*\textbf{where}*)
(*$\cred{\mathsf{fst}}$*) : (*$\A$*)
(*$\cred{\mathsf{snd}}$*) : (*$\B$*) (*$\cred{\mathsf{fst}}$*)
\end{lstlisting}
\end{minipage}
We obtain:
\begin{lstlisting}
(*\textbf{record}*) (*$\Sigma\d$*) ((*$\A$*) : (*$\Type$*)) ((*$\A\cblu{'}$*) : (*$\Type\d$*) (*$\A$*)) ((*$\B$*) : (*$\A$*) (*$\to$*) (*$\Type$*)) ((*$\B\cblu{'}$*) : ((*$\A$*) (*$\to$*) (*$\Type$*))(*$\d$*) (*$\B$*))
: (*$\Type\d$*) ((*$\Sigma$*) (*$\A$*) (*$\B$*)) (*\textbf{where}*)
(*$\cred{\mathsf{fst}}\d$*) : (*$\A\d$*) (*$\cred{\mathsf{fst}}$*)
(*$\cred{\mathsf{snd}}\d$*) : ((*$\B$*) (*$\cred{\mathsf{fst}}$*))(*$\d$*) (*$\cred{\mathsf{snd}}$*)
\end{lstlisting}
Applying~\eqref{eq:d-pi-intro} and the similar rule $≡→$, this becomes:
\begin{lstlisting}
(*\textbf{record}*) (*$\Sigma\d$*) ((*$\A$*) : (*$\Type$*)) ((*$\A\cblu{'}$*) : (*$\A$*) (*$\to$*) (*$\Type$*)) ((*$\B$*) : (*$\A$*) (*$\to$*) (*$\Type$*))
((*$\B\cblu{'}$*) : ((*$\x$*) : (*$\A$*)) ((*$\x\cblu{'}$*) : (*$\A\d$*) (*$\x$*)) (*$\to$*) (*$\B$*) (*$\x$*) (*$\to$*) (*$\Type$*))
: ((*$\s$*) : (*$\Sigma$*) (*$\A$*) (*$\B$*)) (*$\to$*) (*$\Type$*)  (*\textbf{where}*)
(*$\cred{\mathsf{fst}}\d$*) : (*$\A\cblu{'}$*) ((*$\cred{\mathsf{fst}}$*) (*$\s$*))
(*$\cred{\mathsf{snd}}\d$*) : (*$\B\cblu{'}$*) ((*$\cred{\mathsf{fst}}$*) (*$\s$*)) (*$\cred{\mathsf{fst}}\d$*) ((*$\cred{\mathsf{snd}}$*) (*$\s$*))
\end{lstlisting}
In a similar way, the above definition of the record type of categories yields:
\begin{lstlisting}
(*\textbf{record}*) (*$\cred{\mathsf{Cat}}\d$*) : ((*$\MC$*) : (*$\cred{\mathsf{Cat}}$*)) (*$\to$*) (*$\Type$*) (*\textbf{where}*)
(*$\cred{\mathsf{ob}}\d$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*) (*$\to$*) (*$\Type$*)
(*$\cred{\mathsf{hom}}\d$*) : ((*$\x$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*)) ((*$\x\cblu{'}$*) : (*$\cred{\mathsf{ob}}\d$*) (*$\x$*)) ((*$\y$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*)) ((*$\y\cblu{'}$*) : (*$\cred{\mathsf{ob}}\d$*) (*$\y$*)) (*$\to$*) (*$\cred{\mathsf{hom}}$*) (*$\MC$*) (*$\x$*) (*$\y$*) (*$\to$*) (*$\Type$*)
(*$\cred{\mathsf{id}}\d$*) : ((*$\x$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*)) ((*$\x\cblu{'}$*) : (*$\cred{\mathsf{ob}}\d$*) (*$\x$*)) (*$\to$*) (*$\cred{\mathsf{hom}}\d$*) (*$\x$*) (*$\x\cblu{'}$*) (*$\x$*) (*$\x\cblu{'}$*) ((*$\cred{\mathsf{id}}$*) (*$\MC$*) (*$\x$*))
(*$\cred{\mathsf{comp}}\d$*) : {(*$\x$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*)} {(*$\x\cblu{'}$*) : (*$\cred{\mathsf{ob}}\d$*) (*$\x$*)} {(*$\y$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*)} {(*$\y\cblu{'}$*) : (*$\cred{\mathsf{ob}}\d$*) (*$\y$*)} {(*$\z$*) : (*$\cred{\mathsf{ob}}$*) (*$\MC$*)}
{(*$\z\cblu{'}$*) : (*$\cred{\mathsf{ob}}\d$*) (*$\z$*)} ((*$\alpha$*) : (*$\cred{\mathsf{hom}}$*) (*$\MC$*) (*$\y$*) (*$\z$*)) ((*$\alpha\cblu{'}$*) : (*$\cred{\mathsf{hom}}\d$*) (*$\y$*) (*$\y\cblu{'}$*) (*$\z$*) (*$\z\cblu{'}$*) (*$\alpha$*)) ((*$\cblu{\beta}$*) : (*$\cred{\mathsf{hom}}$*) (*$\MC$*) (*$\x$*) (*$\y$*))
((*$\cblu{\beta'}$*) : (*$\cred{\mathsf{hom}}\d$*) (*$\x$*) (*$\x\cblu{'}$*) (*$\y$*) (*$\y\cblu{'}$*) (*$\cblu{\beta}$*)) (*$\to$*) (*$\cred{\mathsf{hom}}\d$*) (*$\x$*) (*$\x\cblu{'}$*) (*$\z$*) (*$\z\cblu{'}$*) ((*$\cred{\mathsf{comp}}$*) (*$\MC$*) (*$\alpha$*) (*$\cblu{\beta}$*))
\end{lstlisting}
Thus a displayed category over $\MC$ has a type of objects indexed by those of $\MC$, types of morphisms indexed by pairs of objects-over-objects and by a morphism of $\MC$, identity and composition operations on displayed objects and morphisms that lie strictly over those in $\MC$, and similarly for the axioms.

As observed in~[6], one use of displayed categories is to state definitions such as Grothendieck fibrations in terms of the existence of cartesian liftings strictly over any morphism in $C$, without internalizing definitional equality.
Another is to construct categories and prove their properties in a modular way out of dependent pieces, just as we do for types using $\Sigma$-types and more general records.
It is \emph{`well-known'} by now that any sort of algebro-categorical structure has a \emph{`displayed version'} --- for instance, displayed bicategories were used in~[4] to prove univalence modularly --- but to our knowledge this has not previously been formalised.
Our displayed type theory (dTT) automatically generates the displayed version of any notion definable in type theory; hence the name.

\paragraph{Outline of the paper.}

The rest of this paper has three parts.
In \cref{sec:syntax} we describe the general syntax of dTT, including the modalities, the operation of display (in various different forms), and how they compute.
We do not prove any canonicity or normalization results, but we conjecture that they hold.

In \cref{sec:ssts} we extend the syntax of dTT to define a type $\SST$ of semi-simplicial types.
In fact, we obtain this as a special case of a general notion of \emph{`display coinductive type'}, which is easier to work with abstractly and also includes the displayed versions $\SST\d$, $\SST\d\d$, etc.
Then we explore a few applications, to make the point that this coinductive notion of semi-simplicial type is useful and practical.

Finally, in \cref{sec:semantics} we consider the semantics of dTT.
In particular, we will show that from any model $\MC$ of ordinary dependent type theory with countable inverse limits (roughly as considered in~[18]), we can construct a model of dTT whose discrete mode is $\MC$ and whose simplicial mode is the category of Reedy fibrant augmented semi-simplicial diagrams in $\MC$, and that this model supports display coinductive types including a type $\SST$ of semi-simplicial types.
The underlying ordinary type theory of this model at the simplicial mode is an instance of the inverse diagram models of~[24, 17], but we construct it more explicitly by hand so as to be able to verify the needed formulas for the additional operations of dTT.

In particular, this model shows that although dTT is (apparently) not conservative over ordinary dependent type theory, it isolates exactly what extra infinitary structure is needed to obtain a well-behaved theory for working with semi-simplicial types, which precisely includes the original model at one mode.
In particular, by~[26] any $(\infty,1)$-topos can be presented by a type-theoretic model topos, which is a model of type theory with countable inverse limits, and thus also yields a model of dTT.

\paragraph{Acknowledgements.} We would like to thank Tim Campion for bringing the binary ordering to our attention, via a talk given by Emily Riehl on her joint work with Tim. Astra would also like to thank Emily Riehl for many discussions in the course of weekly advising meetings, and Steve Awodey for hosting her over a two month period at Carnegie Mellon University, during which many ideas regarding the semantics of dTT were developed.
Mike is grateful to Thorsten Altenkirch and Ambrus Kaposi for many useful conversations while developing Higher Observational Type Theory that have also informed this work.

\clearpage

\section{Syntax of dTT}
\label{sec:syntax}

As suggested in the introduction, dTT is based on a modal type theory roughly in the style of~[15, 14], with two modes, one for discrete types and one for (augmented semi-)simplicial types.
It then adds a notion of \emph{`display'} at the simplicial mode that partially internalises unary parametricity.

In addition, the general form of display, which is needed to state the computation rules for simple display, incorporates dependence on an arbitrary telescope (i.e.\ context extension).
Thus, we also have to include a calculus of telescopes in the theory.\footnote{It would probably be possible to collapse this to dependence on a single type, using $\Sigma$-types instead of telescope extension, as in~[2], but this would be unaesthetic and less practical for implementation.}
The fully general calculus of telescopes and display involves a lot of operations, but in syntax and in most models they are all definable from a smaller number of primitives.

This section is organised as follows.
In \cref{subsec:mode-theory} we define the mode theory, which is a 2-category describing the structure of the modal operators.
Then in \cref{subsec:modal-type-theory} we give the rules for the underlying modal type theory, with modalities but not display.

In \cref{sec:tel} we introduce the most basic notions of the telescope calculus: telescopes, partial substitutions (elements of telescopes), and types and terms dependent on a specified telescope (which we call \emph{`meta-abstractions'}).
These basic notions suffice to give the rules for display, defined mutually with a similar but non-indexed operation on telescopes that we call d\'ecalage, in \cref{sec:dd}.

The remaining two sections introduce further operations that are all essentially \emph{`definable'} in terms of the previous ones.
This is not strictly true at the level of algebraic syntax, where telescopes are just an additional sort of a generalised algebraic theory.
But in a model where telescopes are defined to be finite lists of types --- which is an option in any model, both the free syntactic model and in semantic models arising from categories --- the laws satisfied by these operations characterise them uniquely.
Specifically, in \cref{sec:tma2} we introduce meta-abstracted telescopes, telescope concatenation, and $\Pi$-telescopes, and then in \cref{sec:dtel} we introduce display for telescopes, and d\'ecalage for dependent telescopes.
These operations will be used in \cref{sec:ssts} to formulate display coinductive types, including the type of semi-simplicial types.

\subsection{The mode theory} \label{subsec:mode-theory}

We begin with a modal type theory based on the following 2-category $\M$:
\begin{itemize}
\item there are two modes (objects), $\dm$ for \emph{discrete} and $\sm$ for
\emph{simplicial}
\item there are five nonidentity morphisms, forming hom-posets:
\begin{alignat*}{2}
\M(\dm,\dm) &= \set{\id_\dm}&\qquad
\M(\dm,\sm) &= \set{\tri}\\
\M(\sm,\dm) &= \set{ \sq \le \dia }&\qquad
\M(\sm,\sm) &= \set{ \trisq \le \id_\sm \le \tridia }
\end{alignat*}
\item composition is defined by the following tables (plus identity laws)
\[
\begin{array}{cc|cccc}
&& \multicolumn{3}{c}{\cblu{\oldrho}} \\
& \nu \circ \cblu{\oldrho} &  \tri & \tridia & \trisq\\\hline
\multirow{4}{*}{$\nu$}& \dia & \id_\dm  & \dia & \sq \\
& \sq  & \id_\dm  & \dia & \sq \\
& \tridia   & \tri  & \tridia & \trisq \\
& \trisq  & \tri  & \tridia & \trisq
\end{array}
\qquad
\begin{array}{cc|cc}
&& \multicolumn{2}{c}{\cblu{\oldrho}} \\
&\nu \circ \cblu{\oldrho} & \dia & \sq \\\hline
\nu &\tri & \tridia & \trisq
\end{array}
\]
\end{itemize}
Intuitively, $\tri$ takes a discrete type and forms the constant (augmented semi-)simplicial type, while $\dia$ takes the $(\minusone)$-simplices of an (augmented semi-)simplicial type and $\sq$ takes the limit of an (augmented semi-)simplicial diagram.

One verifies that the following adjunctions hold in $\M$:
\begin{mathpar}
\dia \dashv \tri \dashv \sq
\and
\tridia \dashv \trisq
\and
\id_\p \dashv \id_\p
\end{mathpar}
Thus every morphism in $\M$, except for $\dia$ and $\tridia$, has a right
adjoint. We refer to the morphisms $\dia$ and $\tridia$ as \emph{hazardous}, and
the others \emph{safe}. A characterisation of hazardous morphisms is that they
are precisely those morphisms of the form $\cblu{\oldrho} \circ \dia$. It follows that
the hazardous morphisms are a cosieve: if $\nu$ is hazardous and $\mu$ is
arbitrary, then $\mu\circ\nu$ is hazardous. \bbox

\subsection{The modal type theory}
\label{subsec:modal-type-theory}

The basic syntactic structure of dTT follows MTT~[15]. Each mode has
its contexts, substitutions, types, and terms, so we have the following
judgements where $\p$ denotes an arbitrary mode ($\dm$ or $\sm$).
\begin{mathpar}
\Gamma \ctx_\p
\and
\Gamma \vdash_\p \A \type
\and
\Gamma \vdash_\p \t: \A
\and
\theta : \Gamma \Rightarrow_\p \Theta
\end{mathpar}
Formally speaking, the inference rules we will give below for these judgments should be interpreted as defining a Generalised Algebraic Theory with these four generating sorts.
Later, we will also introduce some additional sorts.

\subsubsection{Contexts}
\label{sec:contexts}

Contexts are built up from the empty contexts by extending with modally
annotated variables and applying locks associated to modalities:
\begin{mathpar}
\infer{\p \mode}{\ec_\p \ctx_\p}
\and
\infer{\mu:\p\to \q \\
\Gamma \ctx_\q}{\bkt{\Gamma,~\lock_\mu} \ctx_\p}
\and
\infer{\mu:\p\to \q \\
\Gamma \ctx_\q \\ \Gamma,~\lock_\mu \vdash_\p \A \type}{\bkt{\Gamma,~\x
:^\mu \A} \ctx_\q}
\end{mathpar}
We additionally enforce the functoriality of locking, and the fact that some
locks preserve empty contexts.
\begin{mathpar}
\bkt{\Gamma,~\lock_{\id_\p}} \equiv \Gamma
\and
\bkt{\Gamma,~\lock_\mu,~\lock_\nu} \equiv \bkt{\Gamma,~\lock_{\mu\circ\nu}}
\and
\bkt{\ec_\dm,~\lock_\sq} \equiv \ec_\sm
\and
\bkt{\ec_\sm,~\lock_\tri} \equiv \ec_\dm
\end{mathpar}
In fact, the last equality follows from the other three, since $\bkt{\ec_\sm,~\lock_\tri} = \bkt{\ec_\dm,~\lock_\sq,~\lock_\tri} = \bkt{\ec_\dm,~\lock_{\sq\circ\tri}} = \bkt{\ec_\dm,\lock_{\id_\dm}} = \ec_{\dm}$.
Note that $\lock_\dia$ does \emph{not} preserve empty contexts.

These equalities mean that contexts no longer have a unique presentation using
the above rules. However, there are ways to select a canonical presentation for
any context. One is to interpret the above equalities as directed rewrites and
work with context presentations that are normal for this rewriting system; thus
there are no identity locks, no repeated locks, and (something about empty
contexts). Another way is to require that exactly one lock appears in between
any two variables.

Semantically, each lock is left adjoint to its corresponding modality.
Thus, $\lock_\sq$ is semantically the same as $\tri$, while $\lock_\tri$ is semantically the same as $\dia$.
The other lock, $\lock_\dia$, is not reified internally by a modality: intuitively, it takes a discrete type and makes it an (augmented semi-)simplicial type that is \emph{empty} at all dimensions $\n>\minusone$.

In particular, $\lock_\sq$ and $\lock_\tri$ have the further left adjoints $\lock_\tri$ and $\lock_\dia$, respectively, so that we will be able to represent their modalities $\sq$ and $\tri$ in Fitch-style as in~[14, 27].

As far as $\lock_\dia$ goes, we can say that it is fully faithful and hence an equivalence onto its image, which consists of the simplicial types that are empty in dimensions $\n>\minusone$.
Moreover, since the initial object is strict, this subcategory is a \emph{sieve}: if we have a morphism $\Gamma\to \Delta$ and $\Delta$ lies in this subcategory, then so does $\Gamma$.
Therefore, while $\lock_\dia$ is not a right adjoint, it is a \emph{parametric} right adjoint, so we can still use the method of of~[14] for $\dia$.

However, rather than postulating an uninterpreted parametric left adjoint of $\lock_\dia$ as in~[14], we can use our knowledge about how this left adjoint is defined semantically to give more specific rules.
Specifically, we can identify its domain as the subcategory of contexts in the essential image of $\lock_\dia$, and on that subcategory the left adjoint actually coincides with $\lock_\tri$.
To represent this semantically, we say that an $\sm$-context is \emph{flat} if, intuitively, it contains a $\lock_\dia$ which is not to the left of any $\lock_\tri$.
Formally, flatness is a predicate on contexts (an additional sort of the GAT) characterised by the following rules:
\begin{mathpar}
\infer{\Gamma \ctx_\dm}{(\Gamma,~\lock_\dia) \flat}
\and
\infer{\Gamma \ctx_\sm \\ \Gamma \flat \\ \mu : \p \to \sm \\
\Gamma,~\lock_\mu \vdash_\p \A \type}{(\Gamma,~\x :^\mu \A) \flat}
\end{mathpar}
Semantically, we think of these as the $\sm$-contexts that are empty above dimension $n>\minusone$, on which the parametric left adjoint of $\lock_\dia$ will act as $\lock_\tri$.
(In our actual model we will do something more clever to avoid assuming the existence of strict initial objects.) \bbox

\subsubsection{Substitutions}
\label{sec:substitutions}

These have the following generating rules, which are the same as those given for MTT in~[15] plus the exceptional rule $\key^{\tridia \geq \id_\sm}$, which represents the fact that semantically $\lock_{\tridia}$ acts as the identity on flat contexts.
\begin{mathpar}
\infer{\Gamma \ctx_\p}{\id_\Gamma : \Gamma \Rightarrow_\p \Gamma}
\and
\infer{\Gamma \ctx_\p}{\sqbkt{}: \Gamma \Rightarrow_\p \ec_\p}
\and
\infer{\mu:\p\to \q \\ \Gamma \ctx_\q \\ \Gamma,~\lock_\mu \vdash_\p \A \type}{\weak^{x:^\mu A} : (\Gamma,~x:^\mu A) \Rightarrow_q \Gamma}
\and
\infer{\theta : \Gamma \Rightarrow_\p \Theta \\ \nu : \Theta \Rightarrow_\p \Upsilon}{\nu \circ \theta : \Gamma \Rightarrow_\p \Upsilon}
\and
\infer{\theta : \Gamma \Rightarrow_\q \Theta \\ \Gamma,~\lock_\mu \vdash_\p \t
: \A~\sqbkt{\theta,~\lock_\mu}} {\sqbkt{\theta,~\t} : \Gamma \Rightarrow_\q
\bkt{\Theta,~\x:^\mu \A}}
\and
\infer{\theta : \Gamma \Rightarrow_\q \Theta}{\sqbkt{\theta,~\lock_\mu} : \bkt{\Gamma,~\lock_\mu} \Rightarrow_\p \bkt{\Theta,~\lock_\mu}}
\and
\infer{\mu \leq \nu}{\key^{\mu \leq \nu} : \bkt{\Gamma,~\lock_\nu} \Rightarrow_\p \bkt{\Gamma,~\lock_\mu}}
\and
\infer{\Gamma \flat}{\key^{\tridia \geq \id_\sm} : \Gamma \Rightarrow_\sm \bkt{\Gamma,~\lock_\tridia}}
\end{mathpar}
In practice, it is useful to iterate the weakening rule and combine it with the lock and key rules to obtain the following rule:
\[
\infer{\theta : \Gamma \Rightarrow_\q \Theta \\ \mu \leq \locks(\Upsilon)}{\sqbkt{ \theta,~\weak^{\Upsilon}_\mu}: \bkt{\Gamma,~\Upsilon} \Rightarrow_\p \bkt{\Theta,~\lock_\mu}}
\]
In fact, we will generally use named variables and leave weakening implicit. \bbox

\subsubsection{Types}
\label{sec:types}

These are defined by several classes of type formers, including, at the
most basic level: \emph{$\Pi$-types} (parametrised by a modality, as in MTT), \emph{universes} (at each mode), and \emph{modal operators}.
\begin{mathpar}
\infer{\Gamma,~\lock_\mu \vdash_\p \A \type \\ \Gamma,~\x :^\mu \A \vdash_\q
\B \type}{\Gamma \vdash_\q \bkt{\x :^\mu \A} \to \B \type}
\\
\infer{\ }{\Gamma \vdash_\dm \Disc \type}
\and
\infer{\ }{\Gamma \vdash_\sm \Type \type}
\\
\infer{\Gamma,~\lock_\sq \vdash_\sm \A \type}{\Gamma \vdash_\dm \sq~\A
\type}
\and
\infer{\Gamma,~\lock_\tri \vdash_\dm \A \type}{\Gamma \vdash_\sm \tri~\A
\type}
\and
\infer{\Gamma,~\lock_\dia \vdash_\sm \A \type}{\Gamma \vdash_\dm \dia~\A
\type}
\end{mathpar}
We don't bother with primitive modal operators $\tridia$ or $\trisq$, since they can be obtained up to isomorphism by composing the others.

We will work with Tarski style universes, and thus require a decoding
\begin{mathpar}
\infer{\Gamma \vdash_\dm \A : \Disc}{\Gamma \vdash_\dm \El~\A \type}
\and
\infer{\Gamma \vdash_\sm \A : \Type}{\Gamma \vdash_\sm \El~\A \type}
\end{mathpar}
Finally, we also have types that arise from substitution:
\begin{mathpar}
\infer{\theta : \Gamma \Rightarrow_\p \Theta \\ \Theta \vdash_\p \A \type}{\Gamma \vdash_\p \A~\sqbkt{\theta} \type}
\end{mathpar}
As usual, substitution will be \emph{`eliminable'} in that $\A~\sqbkt{\theta}$ is always equal to something not involving $\sqbkt{\theta}$, but in the GAT presentation it is one of the generating rules like the others. \bbox

\subsubsection{Terms}
\label{sec:terms}

Terms are defined for each class of type former through introduction
and elimination rules. But first, we have variables.
There are two rules for variables: the ordinary one from MTT, and an \emph{`exceptional'} one arising, like the exceptional key $\key^{\tridia \geq \id_\sm}$, from the fact that $\lock_\tridia$ acts as the identity on flat contexts.
\begin{mathpar}
\infer{\mu \leq \locks(\Theta)}{\Gamma,~\x:^\mu \A,~\Theta \vdash_\q \x :
\A~\sqbkt{\id_\Gamma,~\weak^{\x:^\mu \A,~\Theta}_\mu}}
\and
\infer{\Gamma \flat \\ \locks(\Theta) = \id_\sm}{\Gamma,~\x:^\tridia
\A,~\Theta \vdash_\sm \x : \A~\sqbkt{\id_\Gamma,~\weak^{\x:^\tridia \A,~\Theta}_\tridia}~\sqbkt{\key^{\tridia \geq \id_\sm}}}
\end{mathpar}
For $\Pi$-types, we have (as in MTT):
\begin{mathpar}
\infer{\Gamma,~\x:^\mu \A \vdash_\q \t : \B}{\Gamma \vdash_\q \lambda~\x.~\t :
\bkt{\x :^\mu \A} \to \B}
\and
\infer{\Gamma \vdash_\q \f : \bkt{\x :^\mu \A} \to \B \\ \Gamma,~\lock_\mu
\vdash_\p \a : \A}{\Gamma \vdash_\q \f~\a : \B~\sqbkt{\a / \x}}
\end{mathpar}
For universes, we have a coding function:
\begin{mathpar}
\infer{\Gamma \vdash_\dm \A \type}{\Gamma \vdash_\dm \Code~\A : \Disc}
\and
\infer{\Gamma \vdash_\sm \A \type}{\Gamma \vdash_\sm \Code~\A : \Type}
\end{mathpar}
For the modal operators, we have an introduction rule and negative \emph{`Fitch-style'}
elimination rules.
Following~[14], we formulate these using parametric adjoints in the mode theory.
As noted in \cref{subsec:mode-theory}, the safe modalities have actual left adjoints, so their rules simplify as in~[27].
And for $\lock_\dia$, we have observed that its parametric left adjoint is defined on the flat contexts, and on those it coincides with $\lock_\tri$.

\begin{mathpar}
\infer{\Gamma,~\lock_\sq \vdash_\sm \t : \A}{\Gamma \vdash_\dm \sq~\t :
\sq~\A}
\and
\infer{\Gamma,~\lock_\tri \vdash_\dm \t : \A}{\Gamma \vdash_\sm \tri~\t :
\tri~\A}
\and
\infer{\Gamma,~\lock_\dia \vdash_\sm \t : \A}{\Gamma \vdash_\dm \dia~\t :
\dia~\A}
\\
\infer{\Gamma,~\lock_\tri \vdash_\dm \t : \sq~\A}{\Gamma \vdash_\sm \unsq^\A~\t : \A~\sqbkt{\key^{\trisq \leq \id_\sm}}}
\and
\infer{\Gamma,~\lock_\dia \vdash_\sm \t : \tri~\A}{\Gamma \vdash_\dm \untri^\A~\t : \A}
\and
\infer{\Gamma \flat \\ \Gamma,~\lock_\tri \vdash_\dm \t : \dia~\A}{\Gamma \vdash_\sm \undia^\A~\t : \A~\sqbkt{\key^{\tridia \geq \id_\sm}}}
\end{mathpar}
Finally, we have terms that arise from substitution:
\begin{equation*}
\infer{\theta : \Gamma \Rightarrow_\p \Theta \\ \Theta \vdash_\p \t : \A}{\Gamma \vdash_\p \t~\sqbkt{\theta} : \A~\sqbkt{\theta}}
\eqno\sectend
\end{equation*}

\subsection{Telescopes and meta-abstractions, I}
\label{sec:tel}

\subsubsection{Telescopes}
\label{sec:telescopes}

Telescopes are suffixes of contexts, with the restriction that they may not contain locks.
The judgement $\Gamma \vdash_\p \Theta \tel$ denotes that $\Theta$ is a telescope in context $\Gamma$.
Formally, telescopes are an additional sort of the GAT, with formation rules saying that there is an empty one and they can be built by concatenating types.
\begin{mathpar}
\infer{\Gamma \ctx_\p}{\Gamma \vdash_\p \ec_\p \tel}
\and
\infer{\mu:\p\to \q \\
\Gamma \vdash_\q \Theta \tel \\ \Gamma\ext\Theta,~\lock_\mu \vdash_\p \A \type}{\Gamma \vdash_\q \bkt{\Theta,~\x:^\mu \A} \tel}
\end{mathpar}
Just as with ordinary contexts, we regard these rules as generating telescopes \emph{`inductively'}, although this is not formally the case syntactically.
We thus regard some other operation on telescopes as \emph{`defined'} when we specify rules for how it computes on these forms.
This is justified in most models, where we do actually define the judgment of telescopes inductively by the above rules.

For example, the premise of the second rule above requires knowing how to extend a context by a telescope.
We write this with a distinctive notation as $\Gamma\ext\Theta$, from which the reader can infer that $\Theta$ is a telescope.
Since $\ext$ is an operation on contexts, not a constructor of contexts, it computes on the constructors of telescopes:
\begin{mathpar}
\infer{\Gamma \vdash_\p \Theta\tel}{(\Gamma\ext\Theta) \ctx}
\and
(\Gamma\ext\ec_\p) \equiv  \Gamma
\and
(\Gamma\ext(\Theta,~\x:^\mu \A)) \equiv  ((\Gamma\ext\Theta),~\x:^\mu \A)
\end{mathpar}
We consider the operation $\ext$ to be left-associative with the comma.
Thus, for instance, the context $\Gamma\ext\Theta,~\lock_\mu$ in the rule for extending a telescope by a type means $(\Gamma\ext\Theta),~\lock_\mu$.

By a \emph{strict telescope} we mean a telescope without any nontrivially modal variables.
\begin{mathpar}
\infer{\Gamma \ctx_\p}{\Gamma \vdash_\p \ec_\p \stel}
\and
\infer{\Gamma \vdash_\p \Theta \stel \\ \Gamma\ext\Theta \vdash_\p \A \type}{\Gamma \vdash_\p \bkt{\Theta,~\x:^{\id_\p} \A} \stel}
\end{mathpar}
As is evident, we do not distinguish syntactically between general telescopes and strict ones.
That is, we consider strictness to be a mere \emph{property} of a telescope, or alternatively we treat the obvious map from strict telescopes to telescopes as an implicit coercion. \bbox

\subsubsection{Partial substitutions}
\label{sec:part-subst}

These are elements of telescopes: if $\Gamma\vdash \Upsilon\tel$ there is a judgment $\Gamma \vdash \sigma : \Upsilon$.
We can think of $\sigma$ as a substitution $\Gamma \Rightarrow (\Gamma\ext \Upsilon)$ that is the identity on $\Gamma$.
Formally, we specify that they can be built out of terms:
\begin{mathpar}
\infer{\ }{\Gamma \vdash_\p~\sqbkt{}~: \ec_\p}
\and
\infer{\Gamma \vdash_\q \sigma : \Upsilon \\ \Gamma \ext \Upsilon,~\lock_\mu \vdash_\p \A \type \\  \Gamma,~\lock_\mu \vdash_\p \t : \A~\sqbkt{\id_\Gamma\ext\sigma,~\lock_\mu}}{\Gamma \vdash_\q \sqbkt{\sigma,~\t} : \bkt{\Upsilon,~\x :^\mu \A}}
\end{mathpar}
The second rule involves a notion of extending an ordinary substitution by a partial one.
\begin{mathpar}
\infer{\theta : \Gamma \Rightarrow_\q \Delta \\ \Delta \vdash_p \Upsilon \tel \\ \Gamma \vdash_p \sigma : \Upsilon~\sqbkt{\theta}}
{\sqbkt{\theta\ext\sigma} : \Gamma \Rightarrow_q (\Delta \ext \Upsilon)}
\and
\sqbkt{\theta\ext\sqbkt{}} \equiv  \theta
\and
\sqbkt{\theta\ext\sqbkt{\sigma,~\t}} \equiv  \sqbkt{\sqbkt{\theta\ext\sigma},~\t}
\end{mathpar}
This gives a simple way to ensure that partial substitutions are uniquely determined by their components: their equality is detected by equality of the induced substitutions.
\begin{mathpar}
\infer{\Gamma \vdash_\p \sigma : \Upsilon \\ \Gamma \vdash_p \tau : \Upsilon \\ \sqbkt{\id_\Gamma\ext\sigma} \equiv  \sqbkt{\id_\Gamma\ext\tau} : \Gamma \Rightarrow_\p \bkt{\Gamma \ext \Upsilon}}{\Gamma \vdash_\p \sigma \equiv  \tau : \Upsilon}
\end{mathpar}
Note that a partial substitution \emph{does}, in fact, \emph{have} \emph{`components'}: given $\Gamma \vdash_\q \sigma : \bkt{\Upsilon,~\x :^\mu \A}$ we have
\begin{gather*}
\sqbkt{\id_\Gamma\ext\sigma,~\x,~\lock_\mu} : (\Gamma,\lock_\mu) \to (\Gamma\ext\Upsilon,\x:^\mu \A,\lock_\mu) \\
\Gamma\ext\Upsilon,\x:^\mu \A,\lock_\mu \vdash \x : \A\\
\Gamma,\lock_\mu \vdash \x~\sqbkt{\id_\Gamma\ext\sigma,~\x,~\lock_\mu} : \A
\end{gather*}
We also have a notion of weakening for telescopes.  As before, we omit the equations that this must satisfy.
\begin{mathpar}
\infer{\Gamma\vdash \Theta \tel}{\weak^\Theta : (\Gamma\ext \Theta) \Rightarrow \Gamma}
\and
\weak^{\ec} \equiv  \id_\Gamma
\and
\weak^{\Theta,~\x:^\mu \A} \equiv  \weak^\Theta \circ \weak^{\x:^\mu \A}
\eqno\sectend
\end{mathpar}

\subsubsection{Meta-abstracted types and terms}
\label{sec:meta-abstractions}

We now introduce a new judgment form $\Gamma \vdash_\p \A \slfrac{\type}{_{\upsilon:\Upsilon}}$, where $\Gamma \vdash \Upsilon \tel$.
This should be thought of saying that $\A$ is a type depending on the variables $\upsilon$ in $\Upsilon$, i.e.\ belonging to a \emph{`framework-level $\Pi$-type'} $\A : (\upsilon:\Upsilon) \to \mathsf{type}$.
Accordingly, elements of this judgment are introduced by binding and eliminated by application, with a $\beta$ and $\eta$-rule.
\begin{mathpar}
\infer{\Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \A \type}{\Gamma \vdash_\p \dbkt{\A}_{\upsilon:\Upsilon} \slfrac{\type}{_{\upsilon:\Upsilon}}}
\and
\infer{\Gamma \vdash_\p \cA \slfrac{\type}{_\Upsilon} \\ \Gamma \vdash_\p \sigma : \Upsilon}{\Gamma \vdash_\p \cA~\sigma \type}
\and
\infer{\Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \A \type \\ \Gamma \vdash_\p \sigma : \Upsilon}{\Gamma \vdash_\p \dbkt{\A}_{\upsilon:\Upsilon} ~\sigma \equiv  \A~\sqbkt{\id_\Gamma\ext \sigma}}
\and
\infer{\Gamma \vdash_\p \cA \slfrac{\type}{_\Upsilon} \\ \Gamma \vdash_\p \cB \slfrac{\type}{_\Upsilon} \\ \Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \cA~\upsilon \equiv  \cB~\upsilon }{\Gamma \vdash_p \cA \equiv  \cB}
\end{mathpar}
We also regard $\A \slfrac{\type}{_{\upsilon:\Upsilon}}$ as standing in for its own $\Pi$-type \emph{`$(\upsilon:\Upsilon) \to \A~\upsilon$'}.
Thus, such an $\A$ can have its own terms belonging to it, which are also introduced by binding and eliminated by application, with a $\beta$ and $\eta$-rule.
\begin{mathpar}
\infer{\Gamma \vdash_\p \cA \slfrac{\type}{_\Upsilon} \\ \Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \t : \cA~\upsilon}{\Gamma \vdash_\p \dsqbkt{\t}_{\upsilon:\Upsilon} : \dbkt{\A}_{\upsilon:\Upsilon}}
\and
\infer{\Gamma \vdash_\p \cA \slfrac{\type}{_\Upsilon} \\ \Gamma \vdash_\p \ct : \cA \\ \Gamma \vdash_\p \sigma : \Upsilon}{\Gamma \vdash_\p \ct~\sigma~:~\cA~\sigma \type}
\and
\infer{\Gamma \vdash_\p \cA \slfrac{\type}{_\Upsilon} \\ \Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \t : \cA ~\upsilon\\  \Gamma \vdash_\p \sigma : \Upsilon}
{ \Gamma \vdash_\p \dsqbkt{\t}_{\upsilon:\Upsilon} ~ \sigma \equiv  \t~\sqbkt{\id_\Gamma\ext\sigma}}
\and
\infer{\Gamma \vdash_\p \cA \slfrac{\type}{_\Upsilon} \\\Gamma \vdash_\p \ct : \cA \\ \Gamma \vdash_\p \cs : \cA \\ \Gamma\ext (\upsilon : \Upsilon) \vdash_\p \ct~\upsilon \equiv  \cs~\upsilon}{\Gamma \vdash_\p \ct \equiv  \cs}
\eqno\sectend
\end{mathpar}

\subsection{D\'ecalage and displayed types}
\label{sec:dd}

Semantically, the fundamental operation is shifting the dimensions of a simplicial type.
In classical simplicial homotopy theory, this is called \emph{d\'ecalage}:
\[ \bkt{\A\D}_\n = \A_{\n+\cred{1}} \]
The simplicial structure maps of $\A\D$ are a subset of those of $\A$, while the unused ones assemble into a simplicial map $\A\D \to \A$.
When $\A$ is a type at mode $\sm$, we will regard $\A\D$ as the projection from a type $\A\d$ dependent on $\A$; thus we have
\[ \A\D = (\x:\A,~\xp:\A\d~\x) \]
(Semantically, this is validated by the fact that if $\A$ is Reedy fibrant, then the map $\A\D \to \A$ is a Reedy fibration.)
These dependent types $\A\d$, which we call \emph{display}, are our version of the \emph{`logical relations'} assigned to every type by an internal parametricity theory.

\subsubsection{Display for types}
\label{sec:disp-ty}

In contrast to fully internal parametricity theories, because we don't have degeneracies in our cube category, d\'ecalage and display can only be applied in restricted contexts.
In external parametricity, the logical relations apply only to types in the empty context; but our modalities allow us to say more generally that they apply to any \emph{`boxed'} type.
Here by \emph{`box'} we mean not $\sq$ but the corresponding \emph{endofunctor} of the simplicial mode, namely $\trisq$.
Thus, informally display should have the type $\cred{d} : (\A :^\trisq \Type) \to \A \to \Type$, with computability witnesses being assigned by a function $\cred{d} : (\A :^\trisq \Type)( \x :^\trisq \A) \to \A\d~\x$.
If we reformulate these without referring to $\Pi$-types, we obtain the following rules for our basic notion of \emph{displayed type}:
\begin{mathpar}
\infer{\Gamma,~\lock_{\trisq} \vdash_\sm \A \type \\ \Gamma \vdash_\sm \t :
\A~\sqbkt{\key^{\trisq \leq \id_\sm}}}{\Gamma \vdash_\sm \A\d~\t \type}
\and
\infer{\Gamma, \lock_\trisq \vdash_\sm \t : \A}{\Gamma \vdash \t\d :
\A\d~\bkt{\t~\sqbkt{\key^{\trisq \leq \id_\sm}}}}
\end{mathpar}

However, in order to compute with this, we need a version of it that incorporates dependence on a telescope to the right of the lock.
The corresponding action on that telescope is called d\'ecalage. \bbox

\subsubsection{Telescope d\'ecalage}
\label{sec:telescope-decalage}

As noted above, with display $\A\d$ defined as dependent on $\A$, d\'ecalage $\A\D$ is naturally not a single type but a telescope.
It is therefore natural to generalise its \emph{input} to be a telescope also.
This yields an operation that doubles the variables and groups each type with its displayed version, e.g.\
\[(\x:\A,~ \y:\B)\D \equiv  (\x:\A,~ \x\cblu{'}:\A\d~ \x,~ \y:\B,~ \y\cblu{'}:\B\d~ \y).\]
The classical projection from d\'ecalage to the identity, composed of the leftover face maps, becomes an \emph{`evens'} substitution $\Upsilon\D \to \Upsilon$ that throws away the elements of the displayed types (the primed variables in the above example).
\begin{mathpar}
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Upsilon \tel }{\Gamma \vdash_\sm \Upsilon\D \tel}
\and
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Upsilon \tel \\ \Gamma,~\lock_\trisq \vdash_\sm \sigma : \Upsilon }{\Gamma \vdash_\sm \sigma\D : \Upsilon\D}
\\
\infer{\Gamma \vdash_\sm \sigma : \Upsilon\D}{\Gamma \vdash_\sm \sigma\ev : \Upsilon~\sqbkt{\key^{\trisq\le 1}}}
\and
(\sigma\D)\ev \equiv \sigma~\sqbkt{\key^{\trisq\le 1}}
\and
\end{mathpar}
D\'ecalage preserves empty telescopes.
\begin{mathpar}
\ec_\sm\D \equiv \ec_\sm\and
\sqbkt{}\D \equiv \sqbkt{}\and
\sqbkt{}\ev \equiv \sqbkt{}\and
\end{mathpar}
It will also compute on telescopes extended by a type, but we wait to give these rules in \cref{sec:comp-tel-dec}, since they require more structure. \bbox

\subsubsection{Display for meta-abstractions}
\label{sec:displ-meta-abstr}

The more general version of display alluded to above can informally be thought of as having the following rule:
\begin{mathpar}
\text{\textquestiondown}\quad\infer{\Gamma,~\lock_\trisq\ext \Upsilon \vdash A \type}{\Gamma\ext \Upsilon\D, a:A \vdash A\d~a \type} \quad ?
\end{mathpar}
However, this is not a well-behaved rule because the context of the conclusion is not fully general.
There are multiple ways to solve this problem; we will solve it by saying that general display acts on a meta-abstracted type.
\begin{mathpar}
\infer{\Gamma,~\lock_\trisq \vdash_\sm \cA \slfrac{\type}{_\Upsilon}}{\Gamma \vdash_\sm \cA\d \slfrac{\type}{_{\upsilon:\Upsilon\D, \a:\cA\sqbkt{\key^{\trisq\le 1}}~\upsilon\ev}}} \\
\infer{\Gamma,~\lock_\trisq \vdash_\sm \cA \slfrac{\type}{_\Upsilon} \\ \Gamma,~\lock_\trisq \vdash_\sm \ct : \cA}{\Gamma \vdash_\sm \ct\d : \dbkt{\cA\d~\delta~\bkt{\ct~\delta\ev}}_{~\delta~:~\Upsilon\D}}
%% WRONG:
% \infer{\Gamma,~\lock_\trisq \vdash_\sm \cA \slfrac{\type}{_\Upsilon} \\ \Gamma,\lock_\trisq \vdash \sigma : \Upsilon \\ \Gamma,~\lock_\trisq \vdash_\sm \t : \cA~\sigma}
% {\Gamma \vdash_\sm \t\d_{\cA,\sigma} : \cA\d~\sigma\D~(\t~\sqbkt{\key^{\trisq\le 1}})}
\end{mathpar}
In general, this does not reduce to ordinary display, but it does when applied to a \emph{d\'ecalaged} partial substitution.
\begin{mathpar}
\infer{\Gamma,~\lock_\trisq \vdash_\sm \cA \slfrac{\type}{_\Upsilon} \\ \Gamma,~\lock_\trisq \vdash_\sm \sigma : \Upsilon \\ \Gamma \vdash \t : (\cA~\sigma)~\sqbkt{\key^{\trisq\le 1}}}
{\Gamma \vdash \cA\d~\sigma\D~\t \equiv (\cA~\sigma)\d~\t}
\and
\infer{\Gamma,~\lock_\trisq \vdash_\sm \cA \slfrac{\type}{_\Upsilon} \\ \Gamma,~\lock_\trisq \vdash_\sm \sigma : \Upsilon \\ \Gamma,~\lock_\trisq \vdash_\sm \ct : \cA}
{\Gamma \vdash \ct\d~\sigma\D \equiv (\t~\sigma)\d}
\end{mathpar}
In particular, when $\Upsilon\equiv \ec$ these rules say that display for trivial meta-abstractions is equivalent to ordinary display. \bbox

\subsubsection{Computing d\'ecalage}
\label{sec:comp-tel-dec}

Now we can give the rules \emph{`defining'} telescope d\'ecalage on telescopes extended by a variable.
Specifically, when extending by a non-modal variable, we also extend by its displayed version.
But that displayed version needs to depend on $\Theta\D$, so we define it in terms of display for meta-abstractions.
Note that the well-typedness of $\t\d$ in these rules depends on the reduction of meta-abstraction display on displayed partial substitutions.
\begin{align*}
\bkt{\theta:\Theta,~\x : \A}\D
&\equiv \bkt{\theta:\Theta\D,~\x : \A~\sqbkt{\key^{\trisq\le 1} \ext \theta\ev},~\xp : \dbkt{\A}_{\theta:\Theta}\d~\theta~\x} \\
\sqbkt{\sigma,~\t}\D
&\equiv \sqbkt{\sigma\D,~\t,~\t\d}\\
\sqbkt{\sigma,~\t,~\t'}\ev
&\equiv \sqbkt{\sigma\ev,~\t}
\end{align*}

The case of a nontrivially modal variable is actually simpler.
Note that in this case, the modality must be of the form $\tri \circ \mu$.
Recalling that semantically, $\tri$ constructs a constant simplicial type, we should have informally $(\tri\A)\D = \A$, and therefore $(\tri\A)\d$ is trivial.
For an action on types, this would mean that $(\tri\A)\d~\x$ is the unit type; for our current action on telescopes, it means we can just omit the displayed variables.
\begin{align*}
\bkt{\theta:\Theta,~\x :^{\tri \circ \mu} \A}\D
&\equiv \bkt{\theta:\Theta\D,~\x :^{\tri\circ\mu} \A~\sqbkt{\key^{\trisq\le 1} \ext \theta\ev,~\lock_\mu}}\\
\sqbkt{\sigma,~\t}\D
&\equiv \sqbkt{\sigma\D,~\t}\\
\sqbkt{\sigma,~\t}\ev
&\equiv \sqbkt{\sigma\ev,~\t}
\tag*{\bbox}
\end{align*}

\subsubsection{Computing display}
\label{sec:comp-telesc-displ}

Recall from \cref{sec:intro} that we treat display computationally like the identity types of HOTT, so that it computes on the basic type-formers.
Note that the abstracting telescope changes as we compute, so these rules could not be stated for ordinary display alone.

\paragraph{Non-modal $\Pi$-Types}

This rule represents the traditional behavior of parametricity and logical relations on functions: a computability witness for a function says that it preserves computability witnesses.
\begin{align*}
\dbkt{\bkt{\x : \A} \to \B}_{\upsilon:\Upsilon}\d &\equiv \dbkt{\bkt{\x : \A}\bkt{\xp : \A\d~\x} \to \dbkt{\B}_{\upsilon:\Upsilon, \x:\A}\d~\upsilon~\x~\xp~\bkt{\f~\x}}_{\upsilon:\Upsilon\D,~\f:\bkt{\x:\A}\to\B} \\
\dsqbkt{\lambda~\x.~\t}_{\upsilon:\Upsilon}\d &\equiv \dsqbkt{\lambda~\x~\xp.~\dsqbkt{\t}_{\upsilon:\Upsilon, \x:\A}\d~\upsilon~\x~\xp}_{\upsilon:\Upsilon\D} \\
\dsqbkt{\f~\a}_{\upsilon:\Upsilon}\d &\equiv \dsqbkt{\dsqbkt{\f}_{\upsilon:\Upsilon}\d~\upsilon~\a~\bkt{\dbkt{\a}_{\upsilon:\Upsilon}\d~\upsilon}}_{\upsilon:\Upsilon\D}
\end{align*}

\paragraph{Nontrivially modal $\Pi$-Types}

As with d\'ecalage, here we use the fact that display of $\tri$ is trivial.
Note also that here a modal variable appears in the domain of a meta-abstraction.
This is the reason that we cannot restrict to strict telescopes in general.
\begin{align*}
\dbkt{\bkt{\x :^{\tri\circ\mu} \A} \to \B}_{\upsilon:\Upsilon}\d &\equiv \dbkt{\bkt{\x :^{\tri\circ\mu} \A} \to \dbkt{\B}_{\upsilon:\Upsilon, \x:^{\tri\circ\mu}\A}\d~\upsilon~\x~\xp~\bkt{\f~\x}}_{\upsilon:\Upsilon\D,~\f:\bkt{\x:\A}\to\B} \\
\dsqbkt{\lambda~\x.~\t}_{\upsilon:\Upsilon}\d &\equiv \dsqbkt{\lambda~\x.~\dsqbkt{\t}_{\upsilon:\Upsilon, \x:^{\tri\circ\mu}\A}\d~\upsilon~\x}_{\upsilon:\Upsilon\D} \\
\dsqbkt{\f~\a}_{\upsilon:\Upsilon}\d &\equiv \dsqbkt{\dsqbkt{\f}_{\upsilon:\Upsilon}\d~\upsilon~\a}_{\upsilon:\Upsilon\D}
\end{align*}

\paragraph{Universes}

As with $\Pi$-types, this rule represents the traditional behavior of parametricity and logical relations on the universe: a computability witness for a type is a relation on that type.
\begin{align*}
\dbkt{\Type}_{\upsilon:\Upsilon}\d &\equiv \dbkt{\El~\A \to \Type}_{\upsilon:\Upsilon\D, ~\A:\Type} \\
\dsqbkt{\Code~\A}_{\upsilon:\Upsilon}\d &\equiv \dsqbkt{\lambda~\a.~\Code~\bkt{\dbkt{\A}_{\upsilon:\Upsilon}\d~\upsilon~\a}}_{\upsilon:\Upsilon\D} \\
\dbkt{\El~\A}_{\upsilon:\Upsilon}\d &\equiv \dbkt{\El~\bkt{\dsqbkt{\A}_{\upsilon:\Upsilon}\d~\upsilon~\a}}_{\upsilon:\Upsilon\D,~\a:\El\A}
\tag*{\bbox}
\end{align*}

\subsection{Telescopes and meta-abstractions, II}
\label{sec:tma2}

The rules given so far essentially suffice to characterise the basic theory of dTT.
However, in order to formulate our definition of semi-simplicial types, we need a bit more structure.
To this end, in this section we introduce some more operations on telescopes that can be \emph{`defined'} in terms of those already given.

\subsubsection{Meta-abstracted telescopes}
\label{sec:meta-abstr-telesc}

We start with another judgment form $\Gamma \vdash_\p \Phi \slfrac{\tel}{_{\upsilon:\Upsilon}}$ for a telescope dependent on a telescope, with rules entirely analogous to those for types and terms in \cref{sec:meta-abstractions}.
\begin{mathpar}
\infer{\Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \Phi \tel}{\Gamma \vdash_\p \dbkt{\Phi}_{\upsilon:\Upsilon} \slfrac{\tel}{_{\upsilon:\Upsilon}}}
\and
\infer{\Gamma \vdash_\p \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \vdash_\p \sigma : \Upsilon}{\Gamma \vdash_\p \Phi~\sigma \tel}
\and
\infer{\Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \Phi \tel \\ \Gamma \vdash_\p \sigma : \Upsilon}{\Gamma \vdash_\p \dbkt{\Phi}_{\upsilon:\Upsilon} ~\sigma \equiv  \Phi~\sqbkt{\id_\Gamma\ext \sigma}}
\and
\infer{\Gamma \vdash_\p \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \vdash_\p \Psi \slfrac{\tel}{_\Upsilon} \\ \Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \Phi~\upsilon \equiv  \Psi~\upsilon }{\Gamma \vdash_p \Phi \equiv  \Psi}
\and
\infer{\Gamma \vdash_\p \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \t : \Phi~\upsilon}{\Gamma \vdash_\p \dsqbkt{\t}_{\upsilon:\Upsilon} : \dbkt{\Phi}_{\upsilon:\Upsilon}}
\and
\infer{\Gamma \vdash_\p \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \vdash_\p \ct : \Phi \\ \Gamma \vdash_\p \sigma : \Upsilon}{\Gamma \vdash_\p \ct~\sigma~:~\Phi~\sigma \tel}
\and
\infer{\Gamma \vdash_\p \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \ext \bkt{\upsilon:\Upsilon} \vdash_\p \t : \Phi ~\upsilon\\  \Gamma \vdash_\p \sigma : \Upsilon}
{ \Gamma \vdash_p \dsqbkt{\t}_{\upsilon:\Upsilon} ~ \sigma \equiv  \t~\sqbkt{\id_\Gamma\ext\sigma}}
\and
\infer{\Gamma \vdash_\p \Phi \slfrac{\tel}{_\Upsilon} \\\Gamma \vdash_\p \ct : \Phi \\ \Gamma \vdash_\p \cs : \Phi \\ \Gamma\ext (\upsilon : \Upsilon) \vdash_\p \ct~\upsilon \equiv  \cs~\upsilon}{\Gamma \vdash_\p \ct \equiv  \cs}
\eqno\sectend
\end{mathpar}

\subsubsection{Telescope concatenation}
\label{sec:telesc-conc}

Telescope concatenation is not necessary for the syntactic definition of SSTs, but seems to be required for a clean description of the semantics.
It is essentially a $\Sigma$-type for telescopes, which is definitionally associative with context and telescope extension.

\begin{mathpar}
\infer{\Gamma \vdash \Upsilon \tel \\ \Gamma\ext \Upsilon \vdash \Phi \tel}{\Gamma \vdash (\Upsilon\ext\Phi) \tel}
\and
\infer{\Gamma \vdash \sigma : \Upsilon \\ \Gamma \vdash \delta : \Phi~\sqbkt{\id_\Gamma\ext\sigma}}
{\Gamma \vdash \sqbkt{\sigma\ext\delta} : (\Upsilon\ext\Phi)}
\and
\infer{\Gamma \vdash \theta : (\Upsilon\ext\Phi)}{\Gamma \vdash \theta_\cred{0} : \Upsilon}
\and
\infer{\Gamma \vdash \theta : (\Upsilon\ext\Phi)}{\Gamma \vdash \theta_\cred{1} : \Phi~\theta_\cred{0}}
\and
\sqbkt{\sigma\ext\delta}_\cred{0} \equiv \sigma
\and
\sqbkt{\sigma\ext\delta}_\cred{1} \equiv \delta
\and
\sqbkt{\theta_\cred{0}\ext \theta_\cred{1}} \equiv \theta
\and
(\Gamma \ext (\Upsilon\ext \Phi)) \equiv ((\Gamma \ext \Upsilon)\ext \Phi)
\and
(\Upsilon \ext \ec) \equiv \Upsilon
\and
(\Upsilon \ext \bkt{\Phi, \x:^\mu \A}) \equiv ((\Upsilon\ext \Phi), \x :^\mu \A)
\eqno\sectend
\end{mathpar}

\subsubsection{$\Pi$-telescopes}
\label{sec:pi-telescopes}

To define the copointed endofunctors whose coalgebras are display inductive types, we will need $\Pi$-telescopes.
For simplicity, we require that the codomain be a strict telescope; this suffices for our application.
The basic rules are just like those for $\Pi$-types.

\begin{mathpar}
\infer{\Gamma \vdash \Upsilon\tel \\ \Gamma\ext(\upsilon:\Upsilon) \vdash \Theta \stel}{\Gamma \vdash (\upsilon:\Upsilon) \to \Theta \stel}
\and
\infer{\Gamma \vdash \Upsilon\tel \\ \Gamma\ext(\upsilon:\Upsilon) \vdash \theta:\Theta}{\Gamma \vdash \lambda~\upsilon.~\theta : (\upsilon:\Upsilon) \to \Theta}
\and
\infer{\Gamma\vdash \delta : (\upsilon:\Upsilon) \to \Theta \\\Gamma \vdash \sigma:\Upsilon}{\Gamma \vdash \delta~\sigma : \Theta~\sqbkt{\id_\Gamma\ext\sigma}}
\and
\infer{\Gamma \vdash \Upsilon\tel \\ \Gamma\ext(\upsilon:\Upsilon) \vdash \theta:\Theta\\\Gamma \vdash \sigma:\Upsilon}{\Gamma\vdash  (\lambda~\upsilon.~\theta)~\sigma \equiv \theta~\sqbkt{\id_\Gamma\ext\sigma}}
\and
\infer{\Gamma\vdash \delta : (\upsilon:\Upsilon) \to \Theta \\ \Gamma\vdash \delta' : (\upsilon:\Upsilon) \to \Theta \\ \Gamma\ext (\upsilon:\Upsilon) \vdash \delta~\upsilon \equiv \delta'~\upsilon}{\Gamma \vdash \delta\equiv \delta'}
\end{mathpar}
In addition, we assert computation laws for $\Pi$-telescopes when the domain or codomain is an extension.
\begin{mathpar}
\infer{\Gamma \vdash \Upsilon\tel}{((\upsilon:\Upsilon)\to \ec) \equiv \ec}
\and
\infer{\Gamma \vdash \Theta\tel}{((\xi:\ec)\to \Theta) \equiv \Theta}
\and
\lambda~\upsilon.~\sqbkt{} \equiv \sqbkt{}
\and
\lambda~(\upsilon:\ec).\theta \equiv \theta
\and
\infer{\Gamma \vdash \Upsilon\tel \\ \Gamma\ext(\upsilon:\Upsilon) \vdash \Theta \stel \\ \Gamma\ext(\upsilon:\Upsilon)\ext(\theta:\Theta)\vdash \B \type}{((\upsilon:\Upsilon) \to (\Theta,~ \y : \B)) \equiv (\delta:(\upsilon:\Upsilon) \to \Theta,~\epsilon:(\upsilon:\Upsilon) \to  \B~\sqbkt{\id_\Gamma\ext\upsilon\ext\delta~\upsilon})}
\and
\lambda~\upsilon.\sqbkt{\theta,~b}
\equiv \sqbkt{\lambda~\upsilon.~\theta,~\lambda~\upsilon.~b}
\and
\infer{\Gamma \vdash_\q \Upsilon\tel \\ \Gamma\ext(\upsilon:\Upsilon),\lock_\mu \vdash_p \A \type \\ \Gamma\ext(\upsilon:\Upsilon), \x:^\mu \A \vdash_\q \Theta \tel}{((\upsilon:\Upsilon,~\x:^\mu \A) \to \Theta) \equiv ((\upsilon:\Upsilon) \to (\x:^\mu \A) \to \Theta)}
\and
\lambda~(\upsilon : (\Upsilon\ext\A)).~\theta
\equiv \lambda~\upsilon.~\lambda~x.~\theta
\and
\infer{\Gamma \vdash \Upsilon\tel \\ \Gamma\ext(\upsilon:\Upsilon) \vdash \Theta \tel \\ \Gamma\ext(\upsilon:\Upsilon)\ext(\theta:\Theta)\vdash \Phi \tel}{((\upsilon:\Upsilon) \to (\Theta\ext\Phi)) \equiv (\delta:(\upsilon:\Upsilon) \to \Theta~\ext~\epsilon:(\upsilon:\Upsilon) \to (\Phi~\sqbkt{\id_\Gamma\ext\upsilon\ext\delta~\upsilon}))}
\and
\lambda~\upsilon.\sqbkt{\theta\ext\phi}
\equiv \sqbkt{\lambda~\upsilon.~\theta\ext \lambda~\upsilon.~\phi}
\end{mathpar}
When telescopes are definitionally lists of types, these rules suffice to compute any $\Pi$-telescope in terms of $\Pi$-types. \bbox

\subsection{Displayed telescopes}
\label{sec:dtel}

The structure in \cref{sec:dd}, with display acting on types and d\'ecalage on telescopes, is sufficient to determine the behavior of display.
However, in practice we will also need a notion of dependent d\'ecalage and display for telescopes.
When telescopes are lists of types, this is determined (like ordinary d\'ecalage) by display for types.

\subsubsection{Meta-abstracted d\'ecalage}
\label{sec:metaabsdec}

\begin{mathpar}
\infer{\Gamma,\lock_{\trisq} \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon}}{\Gamma \vdash_\sm \Phi\D \slfrac{\tel}{_{\Upsilon\D}}}
\and
\infer{\Gamma,\lock_{\trisq} \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma,\lock_{\trisq} \vdash_\sm \tau : \Phi}{\Gamma \vdash_\sm \tau\D : \Phi\D}
\and
\infer{\Gamma,\lock_{\trisq} \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \vdash_\sm \tau : \Phi\D}{\Gamma \vdash_\sm \tau\ev : \dbkt{\Phi~\sqbkt{\key^{\trisq\le 1}}~\upsilon\ev}_{\upsilon:\Upsilon\D}}
\and
\infer{\Gamma,\lock_{\trisq} \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma,\lock_{\trisq} \vdash_\sm \sigma : \Upsilon}{\Gamma \vdash \Phi\D~\sigma\D \equiv (\Phi~\sigma)\D}
\and
\infer{\Gamma,\lock_{\trisq} \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma,\lock_{\trisq} \vdash_\sm \sigma : \Upsilon \\ \Gamma,\lock_{\trisq} \vdash_\sm \tau : \Phi}{\Gamma \vdash \tau\D~\sigma\D \equiv (\tau~\sigma)\D}
\and
\infer{\Gamma,\lock_{\trisq} \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma \vdash_\sm \sigma : \Upsilon\D \\ \Gamma \vdash_\sm \tau : \Phi}{\Gamma \vdash \tau\D\ev~\sigma \equiv \tau~\sigma\ev}
\end{mathpar}
We also require that this operation reduce to ordinary d\'ecalage on constant meta-abstractions, and commute appropriately with telescope concatenation, both globally and inside further meta-abstractions.
\begin{mathpar}
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq \vdash \Phi\tel \\ \Gamma \vdash \sigma : \Upsilon\D}{\Gamma \vdash \dbkt{\Phi}_{\Upsilon}\D~\sigma \equiv \Phi\D}
\and
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq \vdash \Phi\tel \\ \Gamma \vdash \sigma : \Upsilon\D \\ \Gamma \vdash \delta : \Phi}{\Gamma \vdash \dsqbkt{\delta}_{\Upsilon}\D~\sigma \equiv \delta\D}
\\
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq\ext \Upsilon \vdash \Phi\tel}
{(\Upsilon\ext\Phi)\D \equiv \left((\upsilon:\Upsilon\D) \ext \dbkt{\Phi}_{\upsilon:\Upsilon}\D~\upsilon\right)}
\and
\infer{\Gamma,\lock_\trisq \vdash \sigma : \Upsilon \\ \Gamma, \lock_\trisq \vdash \delta : \Phi\sqbkt{\id_\Gamma,\lock_\trisq\ext \sigma}}
{\sqbkt{\sigma \ext \delta}\D \equiv \sqbkt{\sigma\D\ext \delta\D}}
\\
\infer{\Gamma,\lock_\trisq\ext\Theta \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq\ext\Theta\ext \Upsilon \vdash \Phi\tel}
{\dbkt{(\Upsilon\ext\Phi)}_\Theta\D \equiv \dbkt{(\upsilon:\dbkt{\Upsilon}_{\theta:\Theta}\D~\theta) \ext \dbkt{\Phi}_{\theta:\Theta,\upsilon:\Upsilon}\D~\theta~\upsilon}_{\theta:\Theta\D}}
\and
\infer{\Gamma,\lock_\trisq\ext\Theta \vdash \sigma : \Upsilon \\ \Gamma, \lock_\trisq\ext\Theta \vdash \delta : \Phi\sqbkt{\id_\Gamma,\lock_\trisq\ext\id_\Theta\ext \sigma}}
{\dsqbkt{\sigma \ext \delta}_\Theta\D \equiv \dsqbkt{\dsqbkt{\sigma}_\Theta\D~\theta \ext \dsqbkt{\delta}_\Theta\D~\theta}_{\theta:\Theta\D}}
\end{mathpar}
Note that in the third equation we have to meta-abstract $\Phi$ in order to apply d\'ecalage, since $\Phi$ itself is not in a $\trisq$-locked context.
In the fourth equation, $\delta\D$ is supposed to inhabit $\dbkt{\Phi}_{\upsilon:\Upsilon}\D~\sigma\D$, but by an equation above this is equal to $(\Phi\sqbkt{\id_\Gamma\ext \sigma})\D$, which is the natural type of $\delta\D$.
The last two equations are similar.

\begin{remark}\label{rmk:acks}
The rules for telescope d\'ecalage from \cref{sec:telescope-decalage} and this section should be compared with the \emph{`local theory'} from~[2], with telescopes and telescope concatenation replacing types and $\Sigma$-types.
The $\Upsilon\D$ from \cref{sec:telescope-decalage} corresponds to their $\forall\A$, while the $\dbkt{\Phi}_{\Upsilon}\D$ from this section corresponds to their $\forall\!\cblu{d} (\x.\B)$.
The $\sigma\D$ from \cref{sec:telescope-decalage} corresponds to their $R$ (although with an added modal lock), while the $\dsqbkt{\delta}_\Upsilon\D$ from this section corresponds to their $\mathrm{\cred{apd}}$ (with modal lock).
We don't have their $\mathrm{\cred{ap}}$ represented explicitly, but one of their rules says it is equivalent to $\mathrm{\cred{apd}}$ in a constant family.
Our $\ev$ is their $\cblu{k}$ (in the unary case, so $\cblu{k}=\cred{0}$), and we do not have their $\S$; as discussed before, the modal guards make symmetry unnecessary.
And, of course, we don't have $\Pi$-telescopes or a universe; we have those only for display, which is indexed. \bbox
\end{remark}

\subsubsection{Computing meta-abstracted d\'ecalage}
\label{sec:comp-metaabsdec}

Like ordinary d\'ecalage, meta-abstracted d\'ecalage computes on telescopes that are made out of types.

\begin{align*}
\dbkt{\theta:\Theta,~\x :^{\tri \circ \mu} \A}_{\upsilon:\Upsilon} \D
&\equiv \dbkt{\theta:\dbkt{\Theta}_{\upsilon:\Upsilon}\D~\upsilon,~\x :^{\tri\circ\mu} \A~\sqbkt{\key^{\trisq\le 1} \ext\upsilon\ev \ext \theta\ev~\upsilon,~\lock_\mu}}_{\upsilon:\Upsilon\D}\\
\dsqbkt{\sigma,~\t}_{\upsilon:\Upsilon}\D
&\equiv \dsqbkt{\dsqbkt{\sigma}_{\upsilon:\Upsilon}\D~\upsilon,~\dsqbkt{\t}_{\upsilon:\Upsilon}~\upsilon\ev}_{\upsilon:\Upsilon\D}\\
\dsqbkt{\sigma,~\t}_{\upsilon:\Upsilon\D}\ev
&\equiv \dsqbkt{\sigma\ev~\upsilon\D,~\t~\upsilon\D}_{\upsilon:\Upsilon}\\
\dbkt{\theta:\Theta,~\x : \A}_{\upsilon:\Upsilon}\D
\begin{multlined}[t][0.7\linewidth]
\equiv \dbkt{\theta:\dbkt{\Theta}_{\upsilon:\Upsilon}\D~\upsilon,~\x : \A~\sqbkt{\key^{\trisq\le 1} \ext\upsilon\ev\ext \theta\ev~\upsilon},\\\xp : \dbkt{\A}_{(\upsilon:\Upsilon~\ext~\theta:\Theta)}\d~\upsilon~\theta~\x}_{\upsilon:\Upsilon\D}
\end{multlined}
\\
\dsqbkt{\sigma,~\t}_{\upsilon:\Upsilon}\D
&\equiv \dsqbkt{\dsqbkt{\sigma}_{\upsilon:\Upsilon}\D~\upsilon,~\dsqbkt{\t}_{\upsilon:\Upsilon}~\upsilon\ev,~\dsqbkt{\t}_{\upsilon:\Upsilon}\d~\upsilon}_{\upsilon:\Upsilon\D}\\
\dsqbkt{\sigma,~\t,~\t'}_{\upsilon:\Upsilon}\ev
&\equiv \dsqbkt{\sigma\ev~\upsilon\D,~\t~\upsilon\D}_{\upsilon:\Upsilon}
\tag*{\bbox}
\end{align*}

\subsubsection{Telescope display}
\label{sec:teldisp}

We also need a notion of indexed display for telescopes.
Note that this always gives a \emph{strict} telescope, even if its input is not.
\begin{mathpar}
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Upsilon \tel \\ \Gamma \vdash_\sm \sigma : \Upsilon~\sqbkt{\key^{\trisq\le 1}}}{\Gamma \vdash_\sm (\Upsilon\d~\sigma) \stel}
\and
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Upsilon \tel \\ \Gamma,\lock_\trisq \vdash_\sm \sigma : \Upsilon}{\Gamma \vdash_\sm \sigma\d : (\Upsilon\d~(\sigma~\sqbkt{\key^{\trisq\le 1}}))}
\and
\end{mathpar}
Like d\'ecalage, telescope display computes on telescopes extended by a type:
\begin{align*}
\bkt{\theta:\Theta,~\x :^{\tri \circ \mu} \A}\d~\sqbkt{\sigma,\t}
&\equiv \Theta\d~\sigma\\
\sqbkt{\sigma,~\t}\d
&\equiv \sigma\d\\
\sqbkt{\sigma,~\t}\od
&\equiv \sigma\od\\
\pair{\sqbkt{\sigma,~\t}}{\sigma'}
&\equiv \sqbkt{\pair{\sigma}{\sigma'},~\t}\\
\bkt{\theta:\Theta,~\x : \A}\d~\sqbkt{\sigma,\t}
&\equiv \bkt{\theta:\Theta\d,~\xp : \dbkt{\A}_{\theta:\Theta}\d~\pair{\sigma}{\theta}~\t} \\
\sqbkt{\sigma,~\t}\d
&\equiv \sqbkt{\sigma\d,~\t\d}\\
\sqbkt{\sigma,~\t,~\t'}\od
&\equiv \sqbkt{\sigma\od,~\t'}\\
\pair{\sqbkt{\sigma,~\t}}{\sqbkt{\sigma',~\t'}}
&\equiv \sqbkt{\pair{\sigma}{\sigma'},~\t,~\t'}
\end{align*}

However, this means that compared to d\'ecalage, telescope display reorders the variables.
For instance, we have
\begin{align*}
(\x:\A,~ \y:\B)\D &\equiv  (\x:\A,~ \x\cblu{'}:\A\d~ \x,~ \y:\B,~ \y\cblu{'}:\B\d~ \y)\\
(\x:\A,~ \y:\B)\d &\equiv \dbkt{\x\cblu{'}:\A\d~ \x,~ \y\cblu{'}:\B\d~ \y }_{\x:\A,\;\y:\B}\\
(\x:\A,~ \y:\B) \ext (\x:\A,~ \y:\B)\d &\equiv (\x:\A,~\y:\b,~ \x\cblu{'}:\A\d~ \x,~ \y\cblu{'}:\B\d~ \y)\\
&\neq (\x:\A,~ \y:\B)\D.
\end{align*}
Thus, we instead relate telescope display to d\'ecalage by an \emph{`odds'} operation that picks out the elements of displayed types, and a \emph{`pairing'} operation that interleaves them together, such that evens and odds together form an isomorphism with pairing as inverse.
\begin{mathpar}
\infer{\Gamma \vdash_\sm \sigma : \Upsilon\D}{\Gamma \vdash_\sm \sigma\od : \Upsilon\d~\sigma\ev}
\and
\infer{\Gamma \vdash_\sm \sigma : \Upsilon~\sqbkt{\key^{\trisq\le 1}} \\ \Gamma \vdash_\sm \sigma' : \Upsilon\d~\sigma}{\Gamma \vdash_\sm \pair{\sigma}{\sigma'} : \Upsilon\D}
\\
\sigma \equiv \pair{\sigma\ev}{\sigma\od}
\and
\pair{\sigma}{\sigma'}\ev \equiv \sigma
\and
\pair{\sigma}{\sigma'}\od \equiv \sigma'
\\
(\sigma\D)\od \equiv \sigma\d
\and
\pair{\sigma~\sqbkt{\key^{\trisq\le 1}}}{\sigma\d} \equiv \sigma\D
\\
\ec_\sm\d~\sqbkt{} \equiv \ec_\sm\and
\sqbkt{}\d \equiv \sqbkt{}\and
\sqbkt{}\od \equiv \sqbkt{}\and
\pair{\sqbkt{}}{\sqbkt{}} \equiv \sqbkt{}
\eqno\sectend
\end{mathpar}

\subsubsection{Meta-abstracted telescope display}
\label{sec:meta-abstr-displ}

Unsurprisingly, we generalise telescope display to apply to meta-abstracted telescopes as well, with rules combining those of \cref{sec:displ-meta-abstr,sec:teldisp}.
First we have the basic rules:
\begin{mathpar}
\infer{\Gamma,\lock_\trisq \vdash \Phi \slfrac{\tel}{_{\upsilon:\Upsilon}}}{\Gamma \vdash \Phi\d \slfrac{\stel}{_{\upsilon:\Upsilon\D, \phi:\Phi\sqbkt{\key^{\trisq\le 1}}\upsilon\ev}}}
\and
\infer{\Gamma,\lock_\trisq \vdash \Phi \slfrac{\tel}{_{\upsilon:\Upsilon}} \\ \Gamma,\lock_\trisq \vdash \delta : \Phi}{\Gamma \vdash \delta\d: \dbkt{\Phi\d~\upsilon~(\delta~\upsilon\ev)}_{\upsilon:\Upsilon\D}}
\and
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma,~\lock_\trisq \vdash_\sm \sigma : \Upsilon \\ \Gamma \vdash \t : (\Phi~\sigma)~\sqbkt{\key^{\trisq\le 1}}}
{\Gamma \vdash \Phi\d~\sigma\D~\t \equiv (\Phi~\sigma)\d~\t}
\and
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Phi \slfrac{\tel}{_\Upsilon} \\ \Gamma,~\lock_\trisq \vdash_\sm \sigma : \Upsilon \\ \Gamma,~\lock_\trisq \vdash_\sm \ct : \Phi}
{\Gamma \vdash \ct\d~\sigma\D \equiv (\t~\sigma)\d}
\end{mathpar}
Then we have the odds/pairing isomorphism:
\begin{mathpar}
\infer{\Gamma,\lock_\trisq \vdash \Phi \slfrac{\tel}{_{\upsilon:\Upsilon}}\\ \Gamma \vdash \delta : \Phi\D}{\Gamma \vdash \delta\od : \dbkt{\Phi\d~\upsilon~  (\delta\ev~\upsilon)}_{\upsilon:\Upsilon\D}}
\and
\infer{\Gamma,\lock_\trisq \vdash \Phi \slfrac{\tel}{_{\upsilon:\Upsilon}} \\
\Gamma \vdash_\sm \delta : \dbkt{\Phi~\sqbkt{\key^{\trisq\le 1}}~\upsilon\ev}_{\upsilon:\Upsilon\D} \\
\Gamma \vdash_\sm \delta' : \dbkt{\Phi\d~\upsilon~(\delta~\upsilon)}_{\upsilon:\Upsilon\D}}
{\Gamma \vdash_\sm \pair{\delta}{\delta'} : \Phi\D}
\\
\delta \equiv \pair{\delta\ev}{\delta\od}
\and
\pair{\delta}{\delta'}\ev \equiv \delta
\and
\pair{\delta}{\delta'}\od \equiv \delta'
\\
(\delta\D)\od \equiv \delta\d
\and
\pair{\delta~\sqbkt{\key^{\trisq\le \id_\sm}}}{\delta\d} \equiv \delta\D
\end{mathpar}
On constant meta-abstractions, this reduces to ordinary telescope display:
\begin{mathpar}
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq \vdash \Phi\tel \\ \Gamma \vdash \sigma : \Upsilon\D \\ \Gamma \vdash \delta : \Phi~\sqbkt{\key^{\trisq\le \id_\sm}\ext \sigma}}{\Gamma \vdash \dbkt{\Phi}_{\Upsilon}\d~\sigma~\delta \equiv \Phi\d~\delta}
\and
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq \vdash \Phi\tel \\ \Gamma \vdash \sigma : \Upsilon\D \\ \Gamma \vdash \delta : \Phi~\sqbkt{\key^{\trisq\le \id_\sm}\ext \sigma}}{\Gamma \vdash \dsqbkt{\delta}_{\Upsilon}\d~\sigma \equiv \delta\d}
\end{mathpar}
And we have computation rules for telescope extensions:
\begin{mathpar}
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq\ext \Upsilon \vdash \Phi\tel\\
\Gamma \vdash \sigma : \Upsilon~\sqbkt{\key^{\trisq\le \id_\sm}} \\ \Gamma \vdash \delta : \Phi~\sqbkt{\key^{\trisq\le \id_\sm}\ext \sigma}}
{(\Upsilon\ext\Phi)\d~\sigma~\delta \equiv \left((\upsilon:\Upsilon\d~\sigma) \ext \dbkt{\Phi}_{\upsilon:\Upsilon}\d~\pair{\sigma}{\upsilon}~\delta\right)}
\and
\infer{\Gamma,\lock_\trisq \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq\ext \Upsilon \vdash \Phi\tel\\
\Gamma,\lock_\trisq \vdash \sigma : \Upsilon \\ \Gamma, \lock_\trisq \vdash \delta : \Phi\sqbkt{\id_\Gamma,\lock_\trisq\ext \sigma}}
{\sqbkt{\sigma \ext \delta}\d \equiv \sqbkt{\sigma\d\ext \delta\d}}
\\
\infer{\Gamma,\lock_\trisq\ext\Theta \vdash \Upsilon\tel \\ \Gamma,\lock_\trisq\ext\Theta\ext \Upsilon \vdash \Phi\tel}
{\dbkt{(\Upsilon\ext\Phi)}_\Theta\d \equiv \dbkt{(\upsilon':\dbkt{\Upsilon}_{\theta:\Theta}\d~\theta~\upsilon) \ext \dbkt{\Phi}_{\theta:\Theta,\upsilon:\Upsilon}\d~\theta~\pair{\upsilon}{\upsilon'}~\phi}_{\theta:\Theta\D,~\upsilon:\Upsilon,~\phi:\Phi}}
\and
\infer{\Gamma,\lock_\trisq\ext\Theta \vdash \sigma : \Upsilon \\ \Gamma, \lock_\trisq\ext\Theta \vdash \delta : \Phi\sqbkt{\id_\Gamma,\lock_\trisq\ext\id_\Theta\ext \sigma}}
{\dsqbkt{\sigma \ext \delta}_\Theta\d \equiv \dsqbkt{\dsqbkt{\sigma}_\Theta\d~\theta \ext \dsqbkt{\delta}_\Theta\d~\theta}_{\theta:\Theta\D}}
\eqno\sectend
\end{mathpar}

\subsubsection{Computing meta-abstracted telescope display}
\label{sec:comp-matd}

These computation rules are again just like the previous ones.
\begin{align*}
\dbkt{\theta:\Theta,~\x :^{\tri \circ \mu} \A}_{\upsilon:\Upsilon}\d~\sqbkt{\sigma,\delta,\t}
&\equiv \Theta\d~\sigma~\delta\\
\dsqbkt{\delta,~\t}_{\upsilon:\Upsilon}\d~\sqbkt{\sigma,\delta,\t}
&\equiv \delta\d~\sigma~\delta\\
\dsqbkt{\delta,~\t}_{\upsilon:\Upsilon}\od
&\equiv \delta\od\\
\pair{\dsqbkt{\delta,~\t}_{\upsilon:\Upsilon\D}}{\delta\cblu{'}}
&\equiv \dsqbkt{\pair{\delta}{\delta\cblu{'}},~\t}_{\upsilon:\Upsilon\D}\\
\dbkt{\theta:\Theta,~\x : \A}_{\upsilon:\Upsilon}\d~\sqbkt{\sigma,\delta,\t}
&\equiv \dbkt{\theta:\Theta\d~\upsilon,~\xp : \dbkt{\A}_{\theta:\Theta}\d~\sigma~\pair{\delta}{\theta}~\t}_{\upsilon:\Upsilon\D} \\
\dsqbkt{\delta,~\t}\d~\sqbkt{\sigma,\delta}
&\equiv \sqbkt{\delta\d~\sigma~\delta,~\t\d~\sigma~\delta}\\
\sqbkt{\delta,~\t,~\t\cblu{'}}\od
&\equiv \sqbkt{\delta\od,~\t\cblu{'}}\\
\pair{\dsqbkt{\delta,~\t}_{\upsilon:\Upsilon}}{\dsqbkt{\delta\cblu{'},~\t\cblu{'}}_{\upsilon:\Upsilon}}
&\equiv \dsqbkt{\pair{\delta}{\delta\cblu{'}},~\t,~\t\cblu{'}}_{\upsilon:\Upsilon\D}
\tag*{\bbox}
\end{align*}

\subsubsection{Computing display on $\Pi$-telescopes}
\label{sec:computing-display-pi}

Finally, we give the following rules for computing display and meta-abstracted display of a $\Pi$-telescope.
These are consistent with the rules for computing display on telescopes extended by a type.
\begin{align*}
((\phi:\Phi) \to \Theta~\phi)\d~\delta
&\equiv (\phi : \Phi\D) \to \Theta\d~\phi\ev~(\delta~\phi\ev)\\
\dbkt{(\phi:\Phi~\upsilon) \to \Theta~\upsilon~\phi}_{\upsilon:\Upsilon}\d
&\equiv \dbkt{(\phi:\Phi\D~\upsilon) \to \Theta\d~\upsilon~\phi~(\delta~\phi\ev)}_{\upsilon:\Upsilon\D, \delta:(\phi:\Phi~\upsilon\ev) \to \Theta~\upsilon\ev~\phi}
\end{align*}
However, it does not seem possible to give rules for computing \emph{d\'ecalage} on a $\Pi$-telescope that are similarly consistent.
Fortunately, we will not need such rules.
Of course, since d\'ecalage and $\Pi$-telescopes both compute independently on telescopes extended by a type, so does their combination.

This concludes our description of the ambient syntax of dTT. \bbox

\section{Semi-simplicial types in dTT}
\label{sec:ssts}

\subsection{Semi-simplicial types}
\label{subsec:semi-simplicial-types}

In an ideal version of displayed type theory, one could define semi-simplicial types as an instance of a general notion of displayed coinductive type.
We would expect to write this in a proof assistant with a syntax like the following, which generalises Agda-like syntax for records by allowing the coinductive input of each destructor to be specified explicitly and referred to in its type.
\begin{lstlisting}
(*\textbf{codata}*) (*$\SST$*) : (*$\Type$*) (*\textbf{where}*)
(*$\Z$*) : (*$\SST$*) (*$\to$*) (*$\Type$*)
(*$\S$*) : ((*$\A$*) : (*$\SST$*)) (*$\to$*) (*$\Z$*) (*$\A$*) (*$\to$*) (*$\SST\d$*) (*$\A$*)
\end{lstlisting}
It is beyond the scope of this paper to give a sufficiently broad framework to generally encompass such definitions, but we will describe one general paradigmatic class of them, analogous to W-types as paradigmatic inductive types and M-types as paradigmatic coinductive types.
However, we begin by discussing the concrete example of $\SST$ in more detail, to help motivate the general case.

\subsubsection{SST basics}
\label{sec:sst-basics}

We begin by giving the type formation law and destructors:
\begin{mathpar}
\infer{\ }{\Gamma \vdash_\sm \SST \type}
\and
\infer{\ }{\Gamma \vdash_\sm \Z : \dbkt{\Type}_{\A\;:\;\SST}}
\and
\infer{\ }{\Gamma \vdash_\sm \S: \dbkt{\SST\d~\A}_{\A\;:\;\SST,\;\a\;:\;\El\;\bkt{\Z\;\A}}}
\end{mathpar}
The constructors are defined as meta-abstractions. We would thus have:
\begin{mathpar}
\Gamma \vdash_\sm \SST\d \slfrac{\type}{_{\A_\ze\;:\;\SST}}
\\
\Gamma \vdash_\sm \Z\d : \dbkt{\El~\bkt{\Z~\A_\ze} \to \Type}_{\set{\A_\ze\;:\;\SST},\;\A_\x\;:\;\SST\d~\A_\ze}
\\
\Gamma \vdash_\sm \S\d : \dbkt{\SST\d\d~\A_\ze~\A_\x~\bkt{\S~\A_\ze~\a_\ze}}_{\set{\A_\ze\;:\;\SST},\;\A_\x\;:\;\SST\d\;\A_\ze,\;\a_\ze\;:\;\El\;\bkt{\Z\;\A_\ze},\;\a_\x\;:\;\El\;\bkt{\Z\d\;\A_\x\;\a_\ze}}
\end{mathpar}
What this calculation suggests is that the family $\SST\d$ should behave as though defined by computing $\d$ on all of the destructors in the code block above:
\begin{lstlisting}
(*\textbf{codata}*) (*$\SST\d$*) : (*$\SST$*) (*$\to$*) (*$\Type$*) (*\textbf{where}*)
(*$\Z\d$*) : {(*$\A_\ze$*) : (*$\SST$*)} (*$\to$*) (*$\SST\d$*) (*$\A$*) (*$\to$*) (*$\Z$*) (*$\A$*) (*$\to$*) (*$\Type$*)
(*$\S\d$*) : {(*$\A_\ze$*) : (*$\SST$*)} ((*$\A_\x$*) : (*$\SST\d$*) (*$\A$*)) ((*$\a_{\ze}$*) : (*$\Z$*) (*$\A_\ze$*)) (*$\to$*) (*$\Z\d$*) (*$\A_\x$*) (*$\a_{\ze}$*) (*$\to$*)
(*$\SST\d\d$*) (*$\A_\ze$*) (*$\A_\x$*) ((*$\S$*) (*$\A_\ze$*) (*$\a_{\ze}$*))
\end{lstlisting}
In general, the types obtained by iterating $\d$ $\n$-times on $\Z$ and $\S$ will begin by taking a $\n$-fold dependent $\SST$ in a generic augmented simplicial context of $\SST$s of lower dependency. This context could be generally inferred from the type of $\n$-fold dependent $\SST$, and we have thus chosen to make those arguments implicit, which would align with the syntactic presentation in the introduction. In particular, the formula for $\A_\cred{2}$ is given by:
\[\Z\d\d~\bkt{\S\d~\bkt{\S~\A~\cblu{x\sub{001}}}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}}} ~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}\]
as opposed to:
\[\Z\d\d~\A~(\S~\A~\cblu{x\sub{001}})~(\S~\A~\cblu{x\sub{010}})~ \bkt{\S\d~\A~\bkt{\S~\A~\cblu{x\sub{001}}}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}}} ~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}. \eqno\bbox\]

\subsubsection{The coinduction principle}
\label{sec:sst-coinduction}

Suppose that we want to construct a function mapping into $\SST$ from a telescope of arbitrary length. We first think purely in terms of code, written in the style of \texttt{Agda}-esque copattern matching, with the goal of writing down something that can conceivably be justified:
\begin{lstlisting}
(*$\f$*) : (*$\X$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\f$*) (*$\t$*)) = ((*\cprime{?$_{\mathsf{Z}_0}$}*) : (*$\Type$*))
(*$\S$*) ((*$\f$*) (*$\t$*)) (*$\a$*) = (*$\f\d$*) (*$\t$*) ((*\cprime{?$_{\mathsf{S}_0}$}*) : (*$\X\d$*) (*$\t$*))

(*$\g$*) : ((*$\t$*) : (*$\X$*)) (*$\to$*) (*$\Y$*) (*$\t$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\g$*) (*$\t$*) (*$\s$*)) = ((*\cprime{?$_{\mathsf{Z}_1}$}*) : (*$\Type$*))
(*$\S$*) ((*$\g$*) (*$\t$*) (*$\s$*)) (*$\a$*) = (*$\g\d$*) (*$\t$*) ((*\cprime{?$_{\mathsf{S}_1}$}*) : (*$\X\d$*) (*$\t$*)) (*$\s$*) ((*\cprime{?$_{\mathsf{S}_2}$}*) : (*$\Y\d$*) (*$\t$*) (*\cprime{?$_{\mathsf{S}_1}$}*) (*$\s$*))
\end{lstlisting}
Here, suppose that $\Gamma,~\lock_\trisq \vdash_\sm \Upsilon \tel$. If we think of $\Upsilon$ as a \emph{state space} and $\sqbkt{\sigma : \Upsilon}$ as a \emph{state}. Then the above definition suggests that we are able to define $\f : \bkt{\upsilon : \Upsilon} \to \SST$ provided that we are able to provide two ingredients. First, we need a way of extracting $\sqbkt{\cred{\widetilde{\Z}}~\sigma : \Type}$, a type of $\cred{0}$-simplices, from a state $\sigma$. Second, we need a way of extracting $\sqbkt{\cred{\widetilde{\S}}~\sigma~\a : \Upsilon\d~\sigma}$, a dependent section of $\Upsilon$ over $\sigma$, from a state $\sigma$ and a $\cred{0}$-simplex $\sqbkt{\a : \cred{\widetilde{\Z}}~\sigma}$. This suggests that a reasonable coinduction principle for $\SST$ is the following:
\begin{mathpar}
\infer{\Gamma,~\lock_\trisq \vdash_\sm \Upsilon \ctx \\ \Gamma,~\lock_\trisq \vdash_\sm \cred{\widetilde{\Z}} : \dbkt{\Type}_{\delta\;:\;\Upsilon} \\ \Gamma,~\lock_\trisq \vdash_\sm \cred{\widetilde{\S}} :  \dbkt{\Upsilon\d~\delta}_{\;\delta\;:\;\Upsilon,\;\a\;:\;\El\;\bkt{\cred{\widetilde{\Z}}\;\delta}}}{\Gamma \vdash_\sm \mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}} : \dbkt{\SST}_{\delta\;:\;\Upsilon}}
\end{mathpar}
The code above also suggests what the computation rules should be:
\begin{align*}
\Z~\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}~\sigma\big) &\equiv \cred{\widetilde{\Z}}~\sigma \\
\S~\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}~\sigma\big)~\a_\ze &\equiv \big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)\d~\pair{\sigma}{\cred{\widetilde{\S}}~\sigma~\a_\ze}
\end{align*}
Now, the expression $\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)\d$ defines a meta abstracted-term of meta-abstracted type $\dbkt{\SST\d~\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}~\upsilon^\cblu{+}\ev\big)}_{\upsilon^\cblu{+}\;:\;\Upsilon\D}$. One reasonable hope is that the display in the above line could be computed in terms of a corecursor for $\SST\d$. However, this approach runs into issues. Towards this aim, let us more generally try to work out the coinduction principle that would let us define $\f : \bkt{\x : \X} \to \SST\d~\bkt{\A~\x}$ for $\Gamma,~\lock_\trisq \vdash_\sm \A : \X \to \SST$. We apply the same methodology as before, and start by writing down reasonable looking code:
\begin{lstlisting}
(*$\f$*) : ((*$\t$*) : (*$\X$*)) (*$\to$*) (*$\SST\d$*) ((*$\A$*) (*$\t$*))
(*$\Z\d$*) ((*$\f$*) (*$\t$*)) (*$\a$*) = ((*\cprime{?$_{\mathsf{Z}_2}$}*) : (*$\Type$*))
(*$\S\d$*) ((*$\f$*) (*$\t$*)) (*$\a$*) (*$\b$*) = (*$\f\d$*) (*$\t$*) ((*\cprime{?$_{\mathsf{S}_3}$}*) : (*$\X\d$*) (*$\t$*))
\end{lstlisting}
However, we then have:
\begin{align*}
\Gamma,~\lock_\trisq,~\t : \X,~\a : \El~\bkt{\Z~\bkt{\A~\t}}, ~\b : \El~\cprime{?_{\mathsf{Z}_2}} &\vdash_\sm \S\d~\bkt{\f~\t}~\a~\b : \SST\d\d ~\bkt{\A~\t}~\bkt{\f~\t}~\bkt{\S~\bkt{\A~\t}~\a} \\
\Gamma,~\lock_\trisq,~\t : \X,~\a : \El~\bkt{\Z~\bkt{\A~\t}}, ~\b : \El~\cprime{?_{\mathsf{Z}_2}} &\vdash_\sm \f\d~\t~\cprime{?_{\mathsf{S}_3}} : \SST\d\d~\bkt{\A~\t}~\bkt{\A\d~\t~\cprime{?_{\mathsf{S}_3}}}~\bkt{\f~\t}
\end{align*}
We see then that there is an index ordering mismatch that seems to prevent us from writing down a coinduction principle for $\SST\d$ corresponding to a simple class of syntactic tricks as above. If dTT were extended to have \emph{symmetries}, then we could make progress here by lining up the $\f~\t$ indices and imposing the definitional equality $\S~\bkt{\A~\t}~\a \equiv \A\d~\t~\cprime{?_{\mathsf{S}_3}}$ as a corecursor premise. On the other hand, without the ability to line up the two $\f~\t$ indicies, trying to instead impose definitional equalities involving $\f$, the very term being defined, creates a vicious cycle, since whether or not a definition of $\f$ is well-typed would depend on checking a definitional equality with $\f$, which presupposes that $\f$ is well-typed. Since, for the present, we have chosen to develop a theory without symmetries, we must abandon this approach.

To salvage this, we will leave $\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)\d$ as a stuck form in the theory, but will specify how to compute $\Z\d$ and $\S\d$ on this normal form. The main idea is that if we define:
\begin{lstlisting}
(*$\f$*) : (*$\X$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\f$*) (*$\t$*)) = (*$\cblu{\mathfrak{z}}$*) (*$\t$*)
(*$\S$*) ((*$\f$*) (*$\t$*)) (*$\a$*) = (*$\f\d$*) (*$\t$*) ((*$\cblu{\mathfrak{s}}$*) (*$\t$*) (*$\a$*))
\end{lstlisting}
then we can compute display on each line of this definition to obtain:
\begin{lstlisting}
(*$\f\d$*) : ((*$\t$*) : (*$\X$*)) (*$\to$*) (*$\X\d$*) (*$\t$*) (*$\to$*) (*$\SST\d$*) ((*$\f$*) (*$\t$*))
(*$\Z\d$*) ((*$\f\d$*) (*$\t$*) (*$\s$*)) = (*$\lambda$*) (*$\a$*) (*$\to$*) (*$\cblu{\mathfrak{z}}\d$*) (*$\t$*) (*$\s$*) (*$\a$*)
(*$\S\d$*) ((*$\f\d$*) (*$\t$*) (*$\s$*)) (*$\cblu{a\sub{0}}$*) (*$\cblu{a\sub{1}}$*) = (*$\f\d\d$*) (*$\t$*) (*$\s$*) ((*$\cblu{\mathfrak{s}}$*) (*$\t$*) (*$\cblu{a\sub{0}}$*)) ((*$\cblu{\mathfrak{s}}\d$*) (*$\t$*) (*$\s$*) (*$\cblu{a\sub{0}}$*) (*$\cblu{a\sub{1}}$*))
\end{lstlisting}
Thus we obtain the computation laws:
\begin{align*}
\Z\d~\big(\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)\d~\sigma^\cblu{+}\big)~\cblu{a} &\equiv \cred{\widetilde{\Z}}\d~\sigma^\cblu{+}~\cblu{a} \\
\S\d~\big(\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)\d~\sigma^\cblu{+}\big)~\cblu{a\sub{0}}~\cblu{a\sub{1}} &\equiv \big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)\d\d~\pair{\sigma^\cblu{+}}{\cred{\widetilde{\S}}\D~\sigma^\cblu{+}~\cblu{a\sub{0}}~\cblu{a\sub{1}}}
\end{align*}
Note that these computation rules were exactly obtained by applying display to both sides of the equation in the initial computation rules. We could iterate this to obtain:
\begin{align*}
\Z^{\cred{\mathsf{d}}^\n} ~\big(\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)^{\cred{\mathsf{d}}^\n}~\sigma^\n\big)~\cblu{\partial}\a &\equiv \cred{\widetilde{\Z}}^{\cred{\mathsf{d}}^\n}~\sigma^\n~\cblu{\partial}\a \\
\S^{\cred{\mathsf{d}}^\n}~\big(\big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)^{\cred{\mathsf{d}}^\n}~\sigma^\n\big)~\cblu{\partial}\a~\a &\equiv \big(\mathsf{\R_\Upsilon}~\cred{\widetilde{\Z}} ~\cred{\widetilde{\S}}\big)^{\cred{\mathsf{d}}^{\n+\cred{1}}}~\pair{\sigma^\n}{\cred{\widetilde{\S}}^{\cred{\mathsf{D}}^\n}~\sigma^\n~\cblu{\partial}\a ~\a}
\end{align*}
The situation on our hands is not unlike that of \texttt{Agda}, where a definition of $\f$ made by (co)pattern matching defines a new normal form and does not expand to a first class intro or elim form when normalised\footnote{The culprit here is not a lack of first-class forms, since \texttt{Agda} has pattern matching lambdas. Rather, the restriction is made primarily to control such runaway unfolding that would substantially affect the performance of type-checking and normalisation. As a consequence, two structurally identical top-level definitions of functions $\f$ and $\g$ made by pattern matching are not definitionally equal.}; such names only reduce when their defining patterns occur. This specific point does not itself inhibit $\textsf{\cred{Nat}}$ canonicity (which \texttt{Cubical Agda} otherwise currently lacks due to its treatment of transport in indexed inductives).

We conjecture that dTT, including its treatment of $\SST$, is fully computational in the sense of $\textsf{\cred{Nat}}$ canonicity, normalization, and decidable typechecking.
More precisely, although this may very well not hold \emph{verbatim} of the theory as written down in this paper, we expect it to hold of a modified presentation fitting within the general framework of ideas.
In particular, while we have presented dTT only as a Generalised Algebraic Theory, all the equations have a clear direction and there are no obvious stuck terms. \bbox

\subsection{Examples of semi-simplicial types}
\label{sec:eg-sst}

Of course, simply \emph{defining} a type of semi-simplicial types is only the first step: we also want to be able to work with such things conveniently.
Developing a full theory of semi-simplicial types is beyond the scope of this paper, but in this section we will give a few examples to suggest that this at least may be possible with our definition of $\SST$ and its corecursion principle.
We will use Agda-esque copattern-matching, and assume that our type theory has plenty of other structure rather than the bare-bones version of dTT that we have studied formally in this paper.

\subsubsection{The singular semi-simplicial types}
\label{subsec:sing}

Thus far we have not discussed propositional equality at all, and the reason for this is that the implementation of display is independent from any implementation of equality, whether that be Martin-L\"of, cubical, or observational. However, we now want to define a semi-simplicial type that arises from the $\infty$-groupoid structure of a type in HoTT.
For concreteness we will do this using a cubical notion of equality, with notation that aligns with \texttt{Cubical Agda}.
In this case, display on path types works as follows:
\begin{align*}
\X : \Type,~\x:\X,~\y:\X &\vdash_\sm \cred{\mathsf{Path}}~\X~\x~\y \\
\begin{multlined}[b][0.6\textwidth]
\X : \Type,~\Y : \X \to \Type,\\\x:\X,~\y:\Y~\x,~\xp:\X,~\yp:\Y~\xp,~ \p:\cred{\mathsf{Path}}~\X~\x~\xp
\end{multlined}
&\vdash_\sm \cred{\mathsf{PathP}} \bkt{\lambda~\cblu{i}.~ \Y~\bkt{\p~\cblu{i}}}~\y~\yp.
\end{align*}
One can work this out using the already provided rules of display, and the information that the path type $\cred{\mathsf{Path}}~\X~\x~\y$ is an alias for the constant dependent path type $\cred{\mathsf{PathP}} \bkt{\lambda~\cblu{i}.~ \X}~\x~\y$.

With this given, the singular semi-simplicial types are defined by corecursion.
Rather than write this explicitly using the corecursor from \cref{subsec:semi-simplicial-types,sec:dcoind}, we use a copattern-matching syntax, including a \emph{`displayed corecursive call'} $\cred{\mathsf{Sing}}\d$.
\begin{lstlisting}
(*$\cred{\mathsf{Sing}}$*) : (*$\Type$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) = (*$\X$*)
(*$\S$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) (*$\x$*) = (*$\cred{\mathsf{Sing}}\d$*) (*$\X$*) ((*$\lambda$*) (*$\y$*) (*$\to$*) (*$\cred{\mathsf{Path}}$*) (*$\X$*) (*$\x$*) (*$\y$*))
\end{lstlisting}
A calculation then yields [with implicit arguments elided]:
\begin{lstlisting}
(*$\Z$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) = (*$\X$*)
(*$\Z\d$*) ((*$\S$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) (*$\cblu{x\sub{01}}$*)) (*$\cblu{x\sub{10}}$*) = (*$\cred{\mathsf{Path}}$*) (*$\X$*) (*$\cblu{x\sub{01}}$*) (*$\cblu{x\sub{10}}$*)
(*$\Z\d\d$*) ((*$\S\d$*) ((*$\S$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) (*$\cblu{x\sub{001}}$*)) (*$\cblu{x\sub{010}}$*) (*$\cblu{\beta\sub{011}}$*)) (*$\cblu{x\sub{100}}$*) (*$\cblu{\beta\sub{101}}$*) (*$\cblu{\beta\sub{110}}$*)
= (*$\cred{\mathsf{PathP}}$*) ((*$\lambda$*) (*$\cblu{i}$*) (*$\to$*) (*$\cred{\mathsf{Path}}$*) (*$\X$*) (*$\cblu{x\sub{001}}$*) (*$\cblu{\beta\sub{110}}$*) (*$\cblu{i}$*)) (*$\cblu{\beta\sub{011}}$*) (*$\cblu{\beta\sub{101}}$*)
(*$\Z\d\d\d$*) ((*$\S\d\d$*) ((*$\S\d$*) ((*$\S$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) (*$\cblu{x\sub{0001}}$*)) (*$\cblu{x\sub{0010}}$*) (*$\cblu{\beta\sub{0011}}$*)) (*$\cblu{x\sub{0100}}$*) (*$\cblu{\beta\sub{0101}}$*) (*$\cblu{\beta\sub{0110}}$*) (*$\cblu{\ff\sub{0111}}$*)) (*$\cblu{x\sub{1000}}$*) (*$\cblu{\beta\sub{1001}}$*) (*$\cblu{\beta\sub{1010}}$*) (*$\cblu{\ff\sub{1011}}$*) (*$\cblu{\beta\sub{1100}}$*) (*$\cblu{\ff\sub{1101}}$*) (*$\cblu{\ff\sub{1110}}$*)
= (*$\cred{\mathsf{PathP}}$*) ((*$\lambda$*) (*$\cblu{i}$*) (*$\to$*) (*$\cred{\mathsf{PathP}}$*) ((*$\lambda$*) (*$\cblu{j}$*) (*$\to$*) (*$\cred{\mathsf{Path}}$*) (*$\X$*) (*$\cblu{x\sub{0001}}$*) (*$\cblu{\ff\sub{1110}}$*) (*$\cblu{i}$*) (*$\cblu{j}$*)) (*$\cblu{\beta\sub{0011}}$*) ((*$\cblu{\ff\sub{1101}}$*) (*$\cblu{i}$*))) (*$\cblu{\ff\sub{0111}}$*) (*$\cblu{\ff\sub{1011}}$*)
\end{lstlisting}

\subsubsection{Nerves of categories}
\label{sec:nerves}

The semi-simplicial nerve of a 1-category can also be defined by corecursion.
Let $\Cat$ denote the type of 1-categories, defined as a record inside dTT (extended by record types), and recall that in \cref{sec:intro} we computed $\Cat\d$ to consist of \emph{`displayed categories'} in the usual sense~[6].
Thus we can define:
\begin{lstlisting}
(*$\cred{\mathsf{Nerve}}$*) : (*$\cred{\mathsf{Cat}}$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\cred{\mathsf{Nerve}}$*) (*$\MC$*)) = (*$\cred{\mathsf{ob}}$*) (*$\MC$*)
(*$\S$*) ((*$\cred{\mathsf{Nerve}}$*) (*$\MC$*)) (*$\x$*) = (*$\cred{\mathsf{Nerve}}\d$*) (*$\MC$*) ((*$\cred{\mathsf{coslice}}$*) (*$\MC$*) (*$\x$*))
\end{lstlisting}
Here for a category $\MC$ and object $\x : \cred{\ob}~\MC$, by $\cred{\mathsf{coslice}}~\MC~\x$ we mean the coslice category $\x/\MC$, regarded as a displayed category over $\MC$ via the forgetful functor.
Note that a definition of $\cred{\mathsf{coslice}} : \bkt{\MC : \cred{\mathsf{Cat}}} \to \cred{\mathsf{ob}}~\MC \to \cred{\mathsf{Cat}}\d~\MC$ at the global level in dTT automatically induces the definition of the dependent coslice $\cred{\mathsf{coslice}}\d$. A similar idea works for bicategories, and any other kind of category for which we can define a displayed (co)slice. \bbox

\subsubsection{Topological singular complexes}
\label{sec:topsing}

In \cref{subsec:sing} we constructed the singular semi-simplicial type associated to the intrinsic $\infty$-groupoid structure of any type.
But we can also construct a more classical singular semi-simplicial set associated to a topological space.
For any type $\cred{\mathsf{Top}}$ of \emph{`topological space'} definable inside of dTT as a record, we have a displayed version $\mathsf{\cred{Top}}\d$.
In some cases, particularly \emph{`nonalgebraic'} ones such as open-set spaces, an element of $\cred{\mathsf{Top}}\d~\X$ is more general than an $\Y:\cred{\mathsf{Top}}$ with a map $\Y\to\X$; but at least \emph{from} such a $\Y$ we can construct its fibers as a displayed space.
Thus, as long as we can construct, for any $\x:\X$, a space of \emph{`continuous paths in $\X$ starting at $\x$'} with an endpoint projection down to $\X$, we can make it a displayed space $\cred{\mathsf{path}}~\X~\x$ over $\X$, and use this to construct the singular semi-simplicial types:
\begin{lstlisting}
(*$\cred{\mathsf{Sing}}$*) : (*$\cred{\mathsf{Top}}$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) = (*$\cred{\mathsf{pt}}$*) (*$\X$*)
(*$\S$*) ((*$\cred{\mathsf{Sing}}$*) (*$\X$*)) (*$\x$*) = (*$\cred{\mathsf{Sing}}\d$*) (*$\X$*) ((*$\cred{\mathsf{paths}}$*) (*$\X$*) (*$\x$*))
\end{lstlisting}

\subsubsection{Fibers and higher spans}
\label{sec:fibers}

As we will see in \cref{sec:semantics}, semantically \emph{each} type at mode $\sm$ is already an augmented semi-simplicial type.
We expect that if we fix a particular $(\minusone)$-simplex in an augmented semi-simplicial type, we should obtain an (unaugmented) semi-simplicial type as its \emph{`fibre'}.
And indeed, we can define this operation:
\begin{lstlisting}
(*$\cred{\mathsf{Fib}}$*) : (*$(\X :^\trisq \Type)$*) ((*$\ze : \X$*)) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\cred{\mathsf{Fib}}$*) (*$\X$*) (*$\ze$*)) = (*$\X\d$*) (*$\ze$*)
(*$\S$*) ((*$\cred{\mathsf{Fib}}$*) (*$\X$*) (*$\ze$*)) (*$\x$*) = (*$\cred{\mathsf{Fib}}\d$*) (*$\X$*) (*$\ze$*) (*$\x$*)
\end{lstlisting}
Note that $\X$ is required to be modal so that we can take display of it.
Then we have, for instance, if $\cblu{\ze\sub{00}}:\X$ and $\cblu{x\sub{01}}, \cblu{x\sub{10}} : \X\d~\cblu{\ze\sub{00}}$,
\begin{align*}
(\cred{\mathsf{Fib}}~\X~\cblu{\ze\sub{00}})_\cred{0} &\equiv \Z~(\cred{\mathsf{Fib}}~\X~\cblu{\ze\sub{00}})\\
&\equiv \X\d~\cblu{\ze\sub{00}}\\
(\cred{\mathsf{Fib}}~\X~\cblu{\ze\sub{00}})_\cred{1}~\cblu{x\sub{01}}~\cblu{x\sub{10}} &\equiv \Z\d~(\S~(\cred{\mathsf{Fib}}~\X~\cblu{\ze\sub{00}})~\cblu{x\sub{01}})~\cblu{x\sub{10}}\\
&\equiv \Z\d~(\cred{\mathsf{Fib}}\d~\X~\cblu{\ze\sub{00}}~\cblu{x\sub{01}})~\cblu{x\sub{10}}\\
&\equiv \X\d\d~\cblu{\ze\sub{00}}~\cblu{x\sub{01}}~\cblu{x\sub{10}}
\end{align*}
and as a last example
\begin{align*}
\Z\d\d~(\S\d~(\S~(\cred{Fib}~\X~\cblu{\ze\sub{000}})~\cblu{x\sub{001}})~\cblu{x\sub{010}}~\cblu{\beta\sub{011}})~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}\\
\Z\d\d~(\S\d~(\cred{Fib}\d~\X~\cblu{\ze\sub{000}}~\cblu{x\sub{001}})~\cblu{x\sub{010}}~\cblu{\beta\sub{011}})~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}\\
\Z\d\d~(\cred{Fib}\d\d~\X~\cblu{\ze\sub{000}}~\cblu{x\sub{001}}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}})~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}\\
\cred{Fib}\d\d~\X~\cblu{\ze\sub{000}}~\cblu{x\sub{001}}~\cblu{x\sub{010}}~\cblu{\beta\sub{011}}~\cblu{x\sub{100}}~\cblu{\beta\sub{101}}~\cblu{\beta\sub{110}}.
\end{align*}
In particular, if we let $\X=\Type$ be the universe and $\ze = \top$ be a unit type, we have
\begin{align*}
(\cred{\mathsf{Fib}}~\Type~\top)_\cred{0} &\equiv \Type\d~\top\\
&\equiv \top \to \Type\\
&\cong \Type\\
(\cred{\mathsf{Fib}}~\Type~\top)_\cred{1}~\cblu{X\sub{01}}~\cblu{X\sub{10}} &\equiv \Type\d\d~\top~\cblu{X\sub{01}}~\cblu{X\sub{10}}\\
&\cong \cblu{X\sub{01}} \to \cblu{X\sub{10}} \to \Type\\
&\equiv \Type\d\d\d~\top~\cblu{X\sub{001}}~\cblu{X\sub{010}}~\cblu{B\sub{011}}~\cblu{X\sub{100}}~\cblu{B\sub{101}}~\cblu{B\sub{110}}\\
\begin{aligned}[t]
&(\cblu{x\sub{001}} : \cblu{X\sub{001}}) (\cblu{x\sub{010}} : \cblu{X\sub{010}}) (\cblu{\beta\sub{011}} : \cblu{B\sub{011}}~\cblu{x\sub{001}}~\cblu{x\sub{010}})\\
&(\cblu{x\sub{100}} : \cblu{X\sub{100}})
(\cblu{\beta\sub{101}} : \cblu{B\sub{101}}~\cblu{x\sub{001}}~\cblu{x\sub{100}})
(\cblu{\beta\sub{110}} : \cblu{B\sub{110}}~\cblu{x\sub{010}}~\cblu{x\sub{100}})\to \Type
\end{aligned}
\end{align*}
Thus $\cred{\mathsf{Fib}}~\Type~\top$ is the semi-simplicial type of types, spans, and a sort of simplicial \emph{`higher spans'} that could also be called \emph{`heterogeneous simplices'}.
More generally, $\cred{\mathsf{Fib}}~\Type~\A$ for any type $\A$ consists of types, spans, and simplicial higher spans indexed by $\A$. \bbox

\subsubsection{Operations on semi-simplicial types}
\label{sec:oper-sst}

We can also use corecursion to define operations on semi-simplicial types that are essentially levelwise.
For instance, any two semi-simplicial types have a product:
\begin{lstlisting}
_(*$\cred\times$*)_ : (*$\SST$*) (*$\to$*) (*$\SST$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\X$*) (*$\cred\times$*) (*$\Y$*)) = (*$\Z$*) (*$\X$*) (*$\cred\times$*) (*$\Z$*) (*$\Y$*)
(*$\S$*) ((*$\X$*) (*$\cred\times$*) (*$\Y$*)) (*$\cred\langle$*) (*$\x$*) (*$\cred{,}$*) (*$\y$*) (*$\cred\rangle$*) = ((*$\S$*) (*$\X$*) (*$\x$*)) (*$\cred{\times\d}$*) ((*$\S$*) (*$\Y$*) (*$\y$*))
\end{lstlisting}
Here in the $\S$ case, we have treated the non-displayed arguments of $\cred{\times\d}$ as implicit: its full type is
\[ \underline{~~}\cred{\times\d}\underline{~~} : \{\X : \SST\} ~(\cblu{X'} : \SST\d~\X)~ \{\Y : \SST\}~ (\cblu{Y'} : \SST\d~\Y) \to \SST\d~(\X\mathbin{\cred{\times}}\Y) \]
There is a similar dependently-typed version, i.e.\ a $\Sigma$-semisimplicial-type:
\begin{lstlisting}
(*$\Sigma$*) : ((*$\X : \SST$*)) (*$\to$*) (*$\SST\d~\X$*) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\Sigma$*) (*$\X$*) (*$\Y$*)) = (*$\Sigma$*) ((*$\Z$*) (*$\X$*)) ((*$\Z\d$*) (*$\Y$*))
(*$\S$*) ((*$\Sigma$*) (*$\X$*) (*$\Y$*)) (*$\cred{\boldsymbol\langle}$*) (*$\x$*) (*$\cred{,}$*) (*$\y$*) (*$\cred{\boldsymbol\rangle}$*) = (*$\Sigma\d$*) ((*$\S$*) (*$\X$*) (*$\x$*)) ((*$\S$*) (*$\Y$*) (*$\y$*))
\end{lstlisting}
There is an empty semi-simplicial type.
Note that the $\S$ case can be omitted, since one of its arguments would belong to the empty type $\cred{\bot}$.
\begin{lstlisting}
(*$\cred{\varnothing}$*) : (*$\SST$*)
(*$\Z$*) (*$\cred{\varnothing}$*) = (*$\cred{\bot}$*)
\end{lstlisting}
Similarly, there is a trivial one:
\begin{lstlisting}
(*$\top$*) : (*$\SST$*)
(*$\Z$*) (*$\top$*) = (*$\top$*)
(*$\S$*) (*$\top$*) (*$\u$*) = (*$\top\d$*)
\end{lstlisting}
We can also take the product of any family of semi-simplicial types indexed by a \emph{discrete} type.
Note that the discreteness of $\A$ means that it doesn't need a displayed version when we apply $\bt\d$ in the $\S$ case.
\begin{lstlisting}
(*$\bt$*) : ((*$\A :^\tri \Type$*)) (*$\to$*) (((*$\a :^\tri \A$*)) (*$\to$*) (*$\SST$*)) (*$\to$*) (*$\SST$*)
(*$\Z$*) ((*$\bt$*) (*$\A$*) (*$\X$*)) = (((*$\a :^\tri \A$*)) (*$\to$*) (*$\Z$*) ((*$\X$*) (*$\a$*)))
(*$\S$*) ((*$\bt$*) (*$\A$*) (*$\X$*)) (*$\p$*) = (*$\bt\d$*) (*$\A$*) (*$\X$*) ((*$\S$*) ((*$\X$*) (*$\a$*)) ((*$\p$*) (*$\a$*)))
\end{lstlisting}

However, there are some things we would naturally expect to be able to define that do not seem possible with our current theory.
For example, the disjoint union of semi-simplicial types should certainly have the disjoint union of $\cred{0}$-simplices, but the slice over a 0-simplex should come only from one of the two sides.
That is, $\S~(\X\cred{+}\Y)~(\cred{\mathsf{inl}}~\x)$ should be morally just $\S~\X~\x$.
However, $\S~\X~\x$ belongs to $\SST\d~\X$, whereas $\S~(\X\cred{+}\Y)~(\cred{\mathsf{inl}}~\x)$ must belong to $\SST\d~(\X\cred{+}\Y)$; thus we need to take its disjoint union with an empty semi-simplicial type displayed over $\Y$.

We defined a \emph{`global'} empty semi-simplicial type above, and it seems intuitively that we should be able to define a \emph{`constant'} version of this displayed over $\Y$.
But as noted in \cref{subsec:semi-simplicial-types,sec:dcoind}, without symmetry it does not seem possible to formulate a useful corecursor for $\SST\d$, and without such a thing it is unclear how to define \emph{`constantly displayed'} semi-simplicial types.
This suggests that further work in this direction might require the addition of symmetries. \bbox

\subsection{Display coinductive types}
\label{sec:dcoind}

Generalizing the discussion of $\SST$, we now formulate a fairly general notion of \emph{`indexed display coinductive type'}.
It depends on a telescope $\Phi$ of `non-uniform parameters', and every element of it has a \emph{`head'} belonging to some specified type family $\A$ and a \emph{`tail'} belonging to the displayed version of the coinductive type itself and depending on a telescope of parameters $\B$.
The idea is analogous to an \emph{`indexed M-type'}, but with the output of the tail being displayed, and with $\B$ being a telescope rather than a simple type.
(The latter change is just to match our informal code more closely, by not requiring all the arguments to be wrapped up in a $\Sigma$-type.)

\begin{mathpar}
\infer{\Gamma, \lock_\trisq \vdash \Phi \tel \\
\Gamma, \lock_\trisq \vdash \A \slfrac{\type}{_{\;\phi\;:\;\Phi}} \\ \Gamma, \lock_\trisq  \vdash \B \slfrac{\tel}{_{\phi\;:\;\Phi,~\x\;:\;\A~\phi}} \\ \Gamma, \lock_\trisq \vdash \sigma : \dbkt{\Phi\d~\phi}_{\;\phi\;:\;\Phi,~ \x\;:\;\A~\phi,~ \y\;:\;\B~\phi~\x}}
{\Gamma \vdash \dCoind_{\bkt{\Phi,\;\A,\;\B,\;\sigma}} \slfrac{\type}{_\Phi} \\
\Gamma \vdash \head_{\bkt{\Phi,\;\A,\;\B,\;\sigma}} : \dbkt{\A~\phi}_{\phi\;:\;\Phi~\sqbkt{\key^{\trisq\le\id}},~ \x\;:\; \dCoind_{\bkt{\Phi,\;\A,\;\B,\;\sigma}}~\phi}\\
\Gamma\vdash \tail_{(\Phi,\;\A,\;\B,\;\sigma)} : \dbkt{\dCoind_{\bkt{\Phi,\;\A,\;\B,\;\sigma}}\d ~\pair{\phi}{\sigma~\phi~\bkt{\head~\x}~\b}~\x}_{\phi,~\x,~\b\;:\;\B~\phi ~\bkt{\head~\phi~\x}}
% \and
% \infer{\Gamma \vdash \phi : \Phi~\sqbkt{\key^{\trisq\le1}} \\ \Gamma \vdash x : \dCoind(\Phi,\A,\B,\sigma)~\phi}{\Gamma \vdash \head~x : \A~{\phi}}
% \and
% \infer{\Gamma \vdash \phi : \Phi~\sqbkt{\key^{\trisq\le1}} \\ \Gamma \vdash x : \dCoind(\Phi,\A,\B,\sigma)~\phi \\ \Gamma \vdash b : \B~\phi~(\head~x)}{\Gamma \vdash \tail~x~b : \dCoind(\Phi,\A,\B,\sigma)\d ~\pair{\phi}{\sigma~(\phi, \head~x, b)}~x }
\and
\infer{\Gamma, \lock_\trisq \vdash \Upsilon \tel \\
\Gamma, \lock_\trisq \vdash \zeta : \dbkt{\Phi}{_{\;\upsilon\;:\;\Upsilon}}\\
\Gamma, \lock_\trisq \vdash \h : \dbkt{\A~{(\zeta~\upsilon)}}_{\;\upsilon\;:\;\Upsilon}\\
\Gamma, \lock_\trisq \vdash \tau : \dbkt{\Upsilon\d~\upsilon}_{\;\upsilon\;:\;\Upsilon,~ \y \;:\; \B~\bkt{\zeta~\upsilon}~\h}\\
\Gamma, \lock_\trisq \ext \upsilon:\Upsilon,~ \y : \B~\bkt{\zeta~\upsilon}~\h \vdash
\zeta\d~\pair{\upsilon}{\tau~\upsilon~\y} \equiv \sigma~(\zeta~\upsilon)~(\h~\upsilon)~\y
{\Gamma \vdash \corec_{\bkt{\Phi,\;\A,\;\B,\;\sigma}}~\bkt{\Upsilon,\;\zeta,\;\h,\;\tau} : \dbkt{\dCoind_{\bkt{\Phi,\;\A,\;\B,\;\sigma}}~(\zeta~\upsilon)}_{\;\upsilon\;:\;\Upsilon} }
\and
\head~(\zeta~\upsilon)~\bkt{\corec_{\bkt{\Phi,\;\A,\;\B,\;\sigma}} ~\bkt{\Upsilon,\;\zeta,\;\h,\;\tau}~\upsilon} \equiv \h~\upsilon
\and
\tail~(\zeta~\upsilon)~\bkt{\corec_{\bkt{\Phi,\;\A,\;\B,\;\sigma}} ~\bkt{\Upsilon,\;\zeta,\;\h,\;\tau}~\upsilon}~\b \equiv \bkt{\corec_{\bkt{\Phi,\;\A,\;\B,\;\sigma}}\bkt{\Upsilon,\;\zeta,\;\h,\;\tau}}\d ~\pair{\upsilon}{\tau~\upsilon~\b}
\end{mathpar}
Now we can define $\SST$ as a particular instance of an indexed display coinductive type (which happens to have trivial indexing).
In fact, it is in some sense the \emph{universal} such instance, where the family $\B$ indexed by $\A$ is the universal family $\El$ indexed by $\Type$.
This may be compared with the fact that the $W$-type of $\El$ is the type of \emph{`presentations of well-founded sets'}~[3], while its $M$-type is the type of \emph{`presentations of ill-founded sets'}~[19].
\begin{equation*}
\SST = \dCoind(\ec, \dbkt{\Type}_{\phi~:~\ec}, \dbkt{\El~\X}_{(\X~:~\Type)}, \dsqbkt{\sqbkt{}}_{(\X~:~\Type,~\x~:~\El~\X)})
\end{equation*}
This is the end of all the primitive rules and definitions we have to give.
From here, we can \emph{deduce} the rules for $\SST$, defining $\Z=\head$ and $\S=\tail$ and $\R=\corec$:
\begin{mathpar}
\infer{ }{\Gamma \vdash \Z : \dbkt{\Type}_{\X~:~\SST}}
\and
\infer{ }{\Gamma \vdash \S : \dbkt{\SST\d~\X}_{\X~:~\SST,~\x~:~\El~(\Z~\X)}}
\and
\infer{\Gamma, \lock_\trisq \vdash \Upsilon \tel \\