\begin{mathpar}
\infer{\mu: \p \to \q \\ \Gamma \ob_{\;{\small\newllbracket}\q{\small\newrrbracket}} \\ \gamma : \Gamma, ~\lock^{\cred{+}}_\mu \vdash_{\;{\small\newllbracket}\p{\small\newrrbracket}} \A~\gamma \type}{\bkt{\gamma : \Gamma, ~\a :^{\mu_\cred{+}} \A~\gamma} \ob_{\;{\small\newllbracket}\q{\small\newrrbracket}}}
\and
\infer{\sigma : \Delta \to_{{\small\newllbracket}\q{\small\newrrbracket}} \Gamma \\ \gamma : \Gamma, ~\lock^{\cred{+}}_\mu \vdash_{\;{\small\newllbracket}\p{\small\newrrbracket}} \t~\gamma : \A~\gamma}{\sqbkt{\sigma,~\t}_{\mu_\cred{+}} : \Delta \to_{{\small\newllbracket}\q{\small\newrrbracket}} \bkt{\gamma : \Gamma, ~\a :^{\mu_\cred{+}} \A~\gamma}}
\end{mathpar}
The case of $\tri_\cred{+}$ is defined as follows, splitting on whether or not $\Gamma$ is flat:
\begin{align*}
\bkt{\gamma : \inf~\Gamma,~\a :^{\tri_\cred{+}} \A~\gamma} &\equiv \inf~\bkt{\gamma : \Gamma,~\a : \A~\gamma}\\
\sqbkt{\inf~\sigma,~\t}_{\tri_\cred{+}} &\equiv \inf~\sqbkt{\sigma, ~\t} \\
\bkt{\gamma : \ins~\Gamma,~\a :^{\tri_\cred{+}} \A~\gamma} &\equiv \ins~\bkt{\gamma : \Gamma,~\a :^\tri \A~\gamma} \\
\sqbkt{\ins~\sigma,~\t}_{\tri_\cred{+}} &\equiv \ins~\sqbkt{\sigma, ~\t}_\tri.
\end{align*}
Following this, the rest of the definitions say that the case of modal extension reduces to extension by a variable or term of modal type:
\begin{align*}
\bkt{\gamma : \Gamma,~\a :^{\dia_\cred{+}} \A~\gamma} &\equiv \bkt{\gamma : \Gamma,~\a : \dia~\A~\gamma} \\
\sqbkt{\sigma,~\t}_{\dia_\cred{+}} &\equiv \sqbkt{\sigma,~\t} \\
\bkt{\gamma : \Gamma,~\a :^{\tridia_\cred{+}} \A~\gamma} &\equiv \bkt{\gamma : \Gamma,~\a :^{\tri_\cred{+}} \dia~\A~\gamma} \\
\sqbkt{\sigma,~\t}_{\tridia_\cred{+}} &\equiv \sqbkt{\sigma,~\t}_{\tri_\cred{+}} \\
\big(\gamma : \Gamma,~\a :^{\sq_\cred{+}} \A~\gamma\big) &\equiv \bkt{\gamma : \Gamma,~\a : \sq~\A~\gamma} \\
\sqbkt{\sigma,~\t}_{\sq_\cred{+}} &\equiv \sqbkt{\sigma,~\t} \\
\big(\gamma : \Gamma,~\a :^{\trisq_\cred{+}} \A~\gamma\big) &\equiv \bkt{\gamma : \Gamma,~\a :^{\tri_\cred{+}} \sq~\A~\gamma} \\
\sqbkt{\sigma,~\t}_{\trisq_\cred{+}} &\equiv \sqbkt{\sigma,~\t}_{\tri_\cred{+}}.
\end{align*}
Each of the context extension operations comes with a notion of parent maps and variables:
\begin{mathpar}
\infer{\gamma : \Gamma,~\lock^{\cred{+}}_\mu \vdash_{\;{\small\newllbracket}\p{\small\newrrbracket}} \A~\gamma \type}{\ft^{\A}_{\mu_\cred{+}} : \big(\gamma : \Gamma,~\a :^{\mu_\cred{+}} \A~\gamma\big) \to \Gamma}
\and
\infer{\gamma : \Gamma,~\lock^{\cred{+}}_\mu \vdash_{\;{\small\newllbracket}\p{\small\newrrbracket}} \A~\gamma \type}{\gamma : \Gamma,~\a :^{\mu_\cred{+}} \A~\gamma,~\lock^{\cred{+}}_\mu \vdash_{\;{\small\newllbracket}\p{\small\newrrbracket}} \zv^{\A}_{\mu_\cred{+}} ~ \gamma~\a : \A^{\sqbkt{\ft^{\A}_{\mu_\cred{+}},\;\lock^{\cred{+}}_\mu}}~\gamma~\a}
\end{mathpar}
For the parent maps $\ft^{\A}_{\tri_\cred{+}}$, we make a definition by cases on whether or not $\Gamma$ is flat:
\[
\ft^{\A}_{\tri_\cred{+}} \equiv
\begin{cases}
\inf~\ft^{\A}_\dm &\text{for} \quad \inf~\Gamma \\
\ins~\ft^{\A}_\tri  &\text{for} \quad \ins~\Gamma.
\end{cases}
\]
The parent maps for $\dia_\cred{+}$ and $\sq_\cred{+}$ reduce to discrete parent maps of variables of modal type:
\begin{align*}
&\ft^{\A}_{\dia_\cred{+}} \equiv \ft^{\dia\A}_\dm
&\ft^{\A}_{\sq_\cred{+}} &\equiv \ft^{\sq\A}_\dm.
\end{align*}
Then, for $\tridia_\cred{+}$ and $\trisq_\cred{+}$, we combine this with the substitution above:
\begin{align*}
&\ft^{\A}_{\tridia_\cred{+}} \equiv \ft^{\dia\A}_{\tri_\cred{+}}
&\ft^{\A}_{\trisq_\cred{+}} \equiv \ft^{\sq\A}_{\tri_\cred{+}}.
\end{align*}
For the zero variables for $\dia_\cred{+}$ and $\sq_\cred{+}$, one checks that the following are well-typed:
\begin{align*}
&\zv^{\A}_{\dia_\cred{+}} \equiv \undia^\A~\zv^{\dia\A}_\dm
&\zv^{\A}_{\sq_\cred{+}} \equiv \unsq^\A~\zv^{\sq\A}_\dm.
\end{align*}
For the zero variables $\zv^{\A}_{\tri_\cred{+}}$, we once again case split:
\[
\zv^{\A}_{\tri_\cred{+}} \equiv
\begin{cases}
\zv^{\A}_\dm &\text{for} \quad \inf~\Gamma \\
\zv^{\A}_\tri  &\text{for} \quad \ins~\Gamma.
\end{cases}
\]
Then, for $\tridia_\cred{+}$ and $\trisq_\cred{+}$, we use $\zv_{\tri_\cred{+}}$:
\begin{align*}
&\zv^{\A}_{\tridia_\cred{+}} \equiv \undia^\A~\zv^{\dia\A}_{\tri_\cred{+}}
&\zv^{\A}_{\trisq_\cred{+}} \equiv \unsq^\A~\zv^{\sq\A}_{\tri_\cred{+}}.
\tag*{\bbox}
\end{align*}

\subsubsection{$\Pi$-Types and Universes}

In the next section, we will construct modal $\Pi$-types. It would however be remiss to not to first mention the construction of \emph{non-modal} $\Pi$-types and universes in $\sm_\cred{+}$. Specifically, we need to say that the non-modal constructs reduce to the respective constructs in $\dm$ and $\sm$, depending on whether or not the context is flat:
\begin{align*}
\cred{\Pi}^{\sm_\cred{+}}~\bkt{\inf~\A}~\bkt{\inf~\B} &\equiv \inf~\bkt{\cred{\Pi}^\dm~\A~\B} \\
\cred{\Pi}^{\sm_\cred{+}}~\bkt{\ins~\A}~\bkt{\ins~\B} &\equiv \ins~\bkt{\cred{\Pi}^\sm~\A~\B} \\
\Type^{\sm_\cred{+}} &\equiv
\begin{cases}
\inf~\Disc &\text{for} \quad \inf~\Gamma \\
\ins~\Type^\sm  &\text{for} \quad \ins~\Gamma.
\end{cases}
\end{align*}
The definitions of $\lambda^{\sm_\cred{+}}$, $\eval^{\sm_\cred{+}}$, $\Code^{\sm_\cred{+}}$, and $\El^{\sm_\cred{+}}$ are similar.

Note that stability under substitution is a more general property in $\sm_\cred{+}$ since we have to additionally consider flat substitutions; if $\inc~\sigma : \inf~\Delta \to \ins~\Gamma$, then we have:
\begin{align*}
&\Big(\cred{\Pi}^{\sm_\cred{+}}~\bkt{\ins~\A}~\bkt{\ins~\B}\Big)^{\inc\;\sigma} \\
&\quad\equiv \Big(\ins~\big(\cred{\Pi}^\sm~\A~\B\big)\Big)^{\inc\;\sigma} \\
&\quad \equiv
\inf~\Big(\big(\cred{\Pi}^\sm~\A~\B\big)_\minusone\Big)^\sigma \\
&\quad \equiv
\inf~\Big(\cred{\Pi}^\dm~\A_\minusone~\B_\minusone\Big)^\sigma \\
&\quad \equiv
\inf~\Big(\cred{\Pi}^\dm~\bkt{\A_\minusone}^\sigma~\bkt{\B_\minusone}^{\mathsf{\cred{W}}_{\cred{2}}^{\A_\minusone}\sigma}\Big) \\
&\quad \equiv
\cred{\Pi}^{\sm_\cred{+}}~\big(\inf~\bkt{\A_\minusone}^\sigma\big)~\big(\inf~\bkt{\B_\minusone}^{\mathsf{\cred{W}}_{\cred{2}}^{\A_\minusone}\sigma}\big) \\
&\quad \equiv
\cred{\Pi}^{\sm_\cred{+}}~\big(\ins~\A\big)^{\inc\;\sigma}~\big(\ins~\B\big)^{\mathsf{\cred{W}}_{\cred{2}}^{\A}\;\bkt{\inc\;\sigma}}
\end{align*}
Similarly for universes:
\begin{align*}
\Big(\Type^{\sm_\cred{+}}\Big)^{\inc\;\sigma} &\equiv \Big(\ins~\Type^\sm\Big)^{\inc\;\sigma} \\
&\quad \equiv \inf~\Big(\bkt{\Type^\sm}_\minusone\Big)^\sigma \\
&\quad \equiv \inf~\Disc^\sigma \\
&\quad \equiv \inf~\Disc \\
&\quad \equiv \Type^{\sm_\cred{+}}
\end{align*}
What makes these calculations work is the relevant constructs have been defined to agree with their discrete counterparts in dimension $\minusone$. \bbox

\subsubsection{Modal $\Pi$-Types}

The last remaining modal construct that we must address is modal $\Pi$-types. These behave according to the following rules:
\begin{mathpar}
\infer{\mu : \p \to \q \\ \gamma : \Gamma, ~\lock^{\cred{+}}_\mu \vdash_{{\small\newllbracket}\p{\small\newrrbracket}} \A~\gamma \type \\ \gamma : \Gamma,~\a :^{\mu_\cred{+}} \A~\gamma \vdash_{{\small\newllbracket}\q{\small\newrrbracket}} \B~\gamma~\a \type}{\gamma : \Gamma \vdash_{{\small\newllbracket}\q{\small\newrrbracket}} \cred{\Pi}^{\sm_\cred{+}}_{\mu}~\A~\B~\gamma \type}
\and
\infer{\gamma : \Gamma, ~\a :^{\mu_\cred{+}} \A~\gamma \vdash_{{\small\newllbracket}\q{\small\newrrbracket}} \t~\gamma~\a : \B~\gamma~\a}{\gamma : \Gamma \vdash_{{\small\newllbracket}\q{\small\newrrbracket}} \lambda^{\sm_\cred{+}}_{\mu}~\t~\gamma : \cred{\Pi}^{\sm_\cred{+}}_{\mu}~\A~\B~\gamma}
\and
\infer{\gamma : \Gamma \vdash_{{\small\newllbracket}\q{\small\newrrbracket}} \f~\gamma :  \cred{\Pi}^{\sm_\cred{+}}_{\mu}~\A~\B~\gamma \\ \gamma : \Gamma, ~\lock^{\cred{+}}_\mu \vdash_{{\small\newllbracket}\p{\small\newrrbracket}} \s~\gamma : \A~\gamma}{\gamma : \Gamma \vdash_{{\small\newllbracket}\q{\small\newrrbracket}} \eval^{\sm_\cred{+}}_{\mu}~\f~\s~\gamma : \B^{\sqbkt{\id_\Gamma,\;\s}_{\mu}}~\gamma}
\end{mathpar}
For $\tri_\cred{+}$ we define:
\begin{align*}
\cred{\Pi}^{\sm_\cred{+}}_{\tri}~\A~\bkt{\ins~\B} &\equiv \ins~\big(\cred{\Pi}^{\sm}_{\tri}~\A~\B\big) \\
\cred{\Pi}^{\sm_\cred{+}}_{\tri}~\A~\bkt{\inf~\B} &\equiv \ins~\big(\cred{\Pi}^{\dm}~\A~\B\big) \\
\lambda^{\sm_\cred{+}}_{\tri}~\bkt{\ins~\t} &\equiv \ins~\big(\lambda^{\sm}_{\tri}~\t\big) \\
\lambda^{\sm_\cred{+}}_{\tri}~\bkt{\inf~\t} &\equiv \inf~\big(\lambda^{\dm}~\t\big) \\
\eval^{\sm_\cred{+}}_{\tri}~\bkt{\ins~\f}~\s &\equiv \ins~\big(\eval^{\sm}_{\tri}~\f~\s\big) \\
\eval^{\sm_\cred{+}}_{\tri}~\bkt{\inf~\f}~\s &\equiv
\inf~\big(\eval^{\dm}~\f~\s\big).
\end{align*}
The other cases reduce to functions of a modal variable:
\begin{align*}
\cred{\Pi}^{\sm_\cred{+}}_{\dia}~\A~\B &\equiv \cred{\Pi}^{\sm_\cred{+}}~\bkt{\dia~\A}~\B \\
\cred{\Pi}^{\sm_\cred{+}}_{\tridia}~\A~\B &\equiv \cred{\Pi}^{\sm_\cred{+}}_{\tri}~\bkt{\dia~\A}~\B \\
\cred{\Pi}^{\sm_\cred{+}}_{\sq}~\A~\B &\equiv \cred{\Pi}^{\sm_\cred{+}}~\bkt{\sq~\A}~\B \\
\cred{\Pi}^{\sm_\cred{+}}_{\trisq}~\A~\B &\equiv \cred{\Pi}^{\sm_\cred{+}}_{\tri}~\bkt{\sq~\A}~\B
\end{align*}
The cases of $\lambda$ and $\eval$ are similar. \bbox

\subsection{Semantics of dTT}
\label{sec:generic-semantics}

Having reviewed the general notion of model for dependent type theory in \cref{sec:categories-with-families}, and constructed our intended model of dTT in \cref{sec:simplicial-model,sec:modal-semantics}, we now describe the general notion of model for dTT.
Of course, since our syntax was presented as a Generalised Algebraic Theory, there is an immediate notion of \emph{model}, namely an algebra for that theory (with algebraic syntax being the initial model).
The point is to reformulate this in more familiar category-theoretic terms.

\subsubsection{Modal structure}
\label{sec:modal-structure}

The general multimodal type theory MTT was presented algebraically in~[15].
We therefore start from this as a baseline and add structure corresponding to our particular theory.

For a general mode 2-category $\M$, the starting point is a \emph{modal context structure}, which is a 2-functor $\C:\M\coop \to \Cat$, where $\M\coop$ denotes reversal of both 1-cells and 2-cells.
The image of a mode $\p$ is the category $\C_\p$ of contexts and substitutions at that mode, and the image of a morphism $\mu:\p\to \q$ is the lock functor $\lock_\mu : \C_\q \to \C_\p$, which we write postfix, $\Gamma \mapsto \Gamma\ce \lock_\mu$.
It is a \emph{modal natural model} if each $\C_\p$ is equipped with a morphism $\pr_\p : \Tm_\p \to \Ty_\p$ in its presheaf category such that for any $\mu:\p\to \q$ the morphism $(\lock_\mu)^*(\pr_\p)$ is representable.
(In particular, taking $\mu=\id_\p$, we see that each $\C_\p$ is an ordinary natural model, hence a CwF.)
This notion encapsulates all the rules for building contexts and substitutions from \cref{subsec:modal-type-theory} except for those that refer to flatness of contexts.

Now, specializing to our mode 2-category from \cref{subsec:mode-theory}, the rules of \cref{subsec:modal-type-theory} say that the flat contexts form a full subcategory of $\C_{\sm}$ that contains the image of $\lock_{\dia}$.
In our algebraic theory we take as primitive the derived rules that a context is flat if and only if it admits a substitution to $(\ec, \lock_{\dia})$, and in that case the latter substitution is unique.
Thus, semantically, $1\ce\lock_{\dia}$ is subterminal and the flat contexts are the slice category $\C_{\sm}/1\ce\lock_{\dia}$.
Since the unit of the adjunction $\lock_{\dia} \dashv \lock_{\tri}$ is an identity, $\lock_\dia$ is fully faithful, and on its image it has $\lock_{\dia}$ as an inverse and therefore also a left adjoint.
In addition, since flat contexts are fixed points (up to isomorphism) of $\lock_{\tridia}$, when $\Gamma$ is flat there is a bijection $\Ty(\Gamma) \cong \Ty(\Gamma\ce\lock_{\tridia})$, and so the modal comprehension $(\Gamma, \x:^{\tridia} \A)$ is isomorphic to an ordinary one $(\Gamma, \x:\A\cblu{'})$.
This justifies the special variable rule and key substitution.
Thus, the following definition encapsulates the judgmental structure of our modal type theory.

\begin{definition}
A \textbf{dTT context structure} is a modal context structure $\C:\M\coop \to \Cat$ in the sense of~[15], where $\M$ is as in \cref{subsec:mode-theory}, such that $1\ce\lock_{\dia}$ is subterminal and the slice category $\C_{\sm}/1\ce \lock_{\dia}$ is the replete image of the fully faithful functor $\lock_{\dia} : \C_\dm \to \C_\sm$.
A \textbf{dTT natural model} is a dTT context structure that is also a modal natural model.
\end{definition}

Next, since our modalities are Fitch-style, their semantics follows~[14].
This requires each functor $\lock_{\mu}$ to \emph{be} a parametric right adjoint and \emph{have} a dependent right adjoint.
However, since each safe $\mu$ is already a right adjoint in $\M$, such $\lock_{\mu}$ are also ordinary (hence parametric) right adjoints.
And since $\lock_{\dia}$ is an equivalence onto a slice category, the inverse of that equivalence is a parametric left adjoint of it.
Thus, to justify our Fitch-style rules for modalities, it suffices to assume the following.

\begin{definition}
A \textbf{dTT modal model} is a dTT natural model such that the functors $\lock_{\dia}$ and $\lock_{\sq}$ have dependent right adjoints.
\end{definition}

Our primary example is, of course, the following.

\begin{theorem}
The simplicial model of \cref{sec:simplicial-model,sec:modal-semantics} is a dTT natural model.
\end{theorem}
\begin{proof}
Of course, we use the extended simplicial model along with the discrete model.
We showed explicitly in \cref{sec:modal-semantics} that this yields a modal context structure for our $\M$.
In the notation of that section, the object $1\ce\lock_{\dia}$ referred to above is $\bkt{\ec,~\lock^{\cred{+}}_\dia} \equiv \inf~\ec$.
The definition of the category $\sm_\cred{+}$ implies immediately that this object is subterminal and its slice category is the replete image (and even the literal image) of $\lock^{\cred{+}}_\dia$.
Finally, in \cref{sec:modal-types} we verified the rules of~[14] for $\dia$ and $\sq$, which as shown in \textit{loc.~cit.} are equivalent to their being dependent right adjoints of $\lock^{\cred{+}}_\dia$ and $\lock^{\cred{+}}_\sq$.
\end{proof}

\subsubsection{Telescopes}
\label{sec:modal-tel}

Modal telescopes generalise ordinary telescopes to modal natural models in a straightforward way.
Let $\M$ be a 2-category.

\begin{definition}
A modal natural model $\C : \M\coop\to\Cat$ \textbf{has telescopes} if it is equipped with:
\begin{itemize}
\item For each $\p\in \M$, a representable natural transformation $\tpr_\p : \PSub_\p \to \Tel_\p$, whose comprehensions we write as $(\gamma:\Gamma \ext \theta: \Theta~\gamma)$.
\item For each $\p$, a morphism of polynomial functors $\ec_\p : \id_{\C_\p} \to \P_{\tpr_\p}$.
\item For any $\mu : \p\to \q$, a morphism of polynomial functors $\P_{\tpr_\q} \circ \P_{\lock_\mu^*  \pr_\p} \to \P_{\tpr_\q}$ that we write as $(\theta:\Theta,~\x:^\mu \A~\theta)$.
\item The rules $(\gamma:\Gamma\ext \ec) = \Gamma$ and $(\gamma:\Gamma\ext(\upsilon:\Upsilon~\gamma,~ \x:^\mu \A~\gamma~\upsilon)) = ((\gamma:\Gamma\ext\upsilon:\Upsilon),~ \x:^\mu \A~\gamma~\upsilon)$ from \cref{sec:telescopes} hold.
\item A morphism of polynomial functors $\P_\tpr \circ \P_\tpr \to \P_\tpr$, which we write as $\Upsilon\ext\Phi$.
(This says how to concatenate telescopes.)
\item The rules $(\gamma:\Gamma \ext (\upsilon:\Upsilon~\gamma \ext \phi:\Phi~\gamma~\upsilon)) = ((\gamma:\Gamma\ext \upsilon:\Upsilon~\gamma) \ext \phi:\Phi~\gamma~\upsilon)$ and $(\upsilon:\Upsilon \ext \ec) = \Upsilon$ and $(\upsilon:\Upsilon \ext (\phi:\Phi~\upsilon,~\x:^\mu \A~\upsilon~\phi)) = ((\upsilon:\Upsilon\ext \phi:\Phi~\upsilon),~ \x:^\mu \A~\upsilon~\phi)$ from \cref{sec:telesc-conc} hold.
\end{itemize}
In addition, we say $\C$ has \textbf{$\Pi$-telescopes} if for each $\p$ there is a pullback square
\[
\begin{tikzcd}
\P_{\tpr_\p}(\PSub_\p) \ar[d,"\P_{\tpr_\p}(\tpr_\p)"']\ar[r]\drpullback & \PSub_\p \ar[d,"\tpr_\p"] \\
\P_{\tpr_\p}(\Tel_\p) \ar[r,"\cred{\Pi}"'] & \Tel_\p,
\end{tikzcd}
\]
such that the computation rules from \cref{sec:pi-telescopes} hold.
\end{definition}

As in \cref{sec:semtel,sec:meta-abs}, we can equip any modal natural model with telescopes and $\Pi$-telescopes, and interpret meta-abstracted types and telescopes automatically, without needing to discuss them explicitly. \bbox

\subsubsection{Display and d\'ecalage}
\label{sec:sem-d}

If $\C$ is a CwF with telescopes and $\Gamma\in \C$, we write $\Telover\Gamma$ for the category whose objects are telescopes $\Theta \in \Tel(\Gamma)$ and whose morphisms are morphisms $(\Gamma\ext \Theta_\cblu{1}) \to (\Gamma\ext \Theta_\cblu{2})$ in $\C/\Gamma$.
Thus, it is equivalent to the full subcategory of $\C/\Gamma$ on objects of the form $\Gamma\ext \Theta$.
We call this \emph{the category of telescopes of $\Gamma$}.
Note that by substitution, it is strictly functorial in $\Gamma$, i.e.\ we have a functor $\Telover- : \C\op \to \Cat$.
Equivalently, therefore, we can regard this as an internal category in the presheaf category $\Set^{\C\op}$.

In fact the category $\Telover\Gamma$ is actually itself a CwF.
Its \emph{`types'} in \emph{`context'} $\Upsilon \in \Telover\Gamma$ are meta-abstracted telescopes $\Gamma \vdash \Phi \slfrac{\tel}{_\Upsilon}$.
These are equivalent (but not equal) to telescopes in an extended context, i.e.\ the elements of $\Tel(\Gamma \ext \Upsilon)$.
Similarly, meta-abstracted partial substitutions $\Gamma \vdash \phi : \Phi$ are equivalent to terms $\Gamma\ext(\upsilon:\Upsilon) \vdash \phi:\Phi~\upsilon$, and semantically to sections of such a projection, $(\Gamma\ext \Upsilon) \to (\Gamma\ext \Upsilon\ext\Phi)$ over $(\Gamma\ext \Upsilon)$.
Comprehension is by telescope concatenation.
Because $\Gamma \ext \ec \equiv \Gamma$, the CwF $\Telover\Gamma$ has the following special property.

\begin{definition}
A CwF $\C$ is \textbf{strongly democratic} if every context is the comprehension of a unique type in the empty context.
\end{definition}

Since all of the structure of $\Telover\Gamma$ is strictly stable under substitution in $\Gamma$, these categories form an internal CwF in the presheaf category $\Set^{\C\op}$.
We call this the \emph{internal telescope model} of $\C$ and denote it $\bTel$.
Recalling \cref{rmk:acks} and comparing to the discussion of the local theory in~[2], we find that the syntactic structure of d\'ecalage from \cref{sec:telescope-decalage,sec:metaabsdec} can be described precisely as an internal CwF morphism.

\begin{definition}\label{def:decalage}
Let $\C : \M\coop\to\Cat$ be a dTT natural model with telescopes.
We say it \textbf{has d\'ecalage} if it is equipped with a strict morphism of internal strongly democratic CwFs
\[(\blank)\D : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm \]
in the category of presheaves over $\C_\sm$, together with an internal natural transformation $\evens$ from $(\blank)\D$ to $(\blank)\sqbkt{\key^{\trisq\le \id_\sm}} : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm$.
\end{definition}

In particular, therefore, this structure ordinary includes functors
\((\blank)\D : \Telover(\Gamma\ce\lock_\trisq) \to \Telover\Gamma\)
and natural transformations $\evens$ consisting of maps
\( (\Gamma\ext \Upsilon\D) \to (\Gamma\ce\lock_\trisq\ext \Upsilon), \)
all strictly stable under pullback.
This, together with the strict preservation of empty contexts by the functor $(\blank)\D$, is what the rules of \cref{sec:telescope-decalage} say.
The corresponding action on \emph{`types'} (meta-abstracted telescopes) and \emph{`terms'} (meta-abstracted partial substitutions) assembles into the rules of \cref{sec:metaabsdec}.

We can phrase display in a similar way by defining an auxiliary internal CwF.
We start with telescope display (\cref{sec:dtel}).
Recall from~[24, 17] that from any CwF $\C$ we can construct a \emph{`Sierpinski'} model $\C^\cred{2}$.
Its objects (contexts) are arbitrary morphisms $\gamma_\cblu{01}: \Gamma_\cred{1} \to \Gamma_\cred{0}$ in $\C$, but its types are pairs of $\A_\cred{0} \in \Ty(\Gamma_\cred{0})$ and $\A_\cred{1} \in \Ty(\Gamma_\cred{1} \ce \A_\cred{0}\sqbkt{\gamma_\cblu{01}})$.
Moreover, there is a strict CwF morphism $(\blank)_\cred{0} : \C^\cred{2} \to \C$, which preserves all the type-formers, in particular $\Sigma$-types if $\C$ has them.
If $\C$ has $\Sigma$-types there is also a functor $(\blank)_\cred{1} : \C^\cred{2} \to \C$ that sends a type $(\A_\cred{0},\A_\cred{1})$ to $\Sigma(\A_\cred{0}\sqbkt{\gamma_\cblu{01}}, \A_\cred{1})\in \Ty(\Gamma_\cred{1})$, but this only preserves comprehension and $\Sigma$-types up to isomorphism.
Thus it is a pseudo CwF morphism in the sense of~\cite[Definition 10]{cd:lccc-tt}, although it preserves substitution and the empty context strictly.

Now let $\C$ be a CwF, and apply this construction internally in the category of presheaves on $\C$ to the internal telescope model $\bTel$.
We thus obtain another CwF $\bTel^\cred{2}$ internal to presheaves, in which the \emph{`contexts'} over $\Gamma$ are morphisms of telescopes $\theta_\cblu{01} : \Theta_\cred{1} \to \Theta_\cred{0}$ over $\Gamma$, and the \emph{`types'} in such a \emph{`context'} over $\Gamma$ are pairs of two telescopes $\Upsilon_\cred{0} \in \Tel(\Gamma\ext\Theta_\cred{0})$ and $\Upsilon_\cred{1} \in \Tel(\Gamma \ext \Theta_\cred{1} \ext \Upsilon_\cred{0}\sqbkt{\theta_\cblu{01}})$.
This is no longer strongly democratic, but as always we have the strict CwF morphism $(\blank)_\cred{0} : \bTel^\cred{2} \to \bTel$ that preserves $\Sigma$-types (i.e.\ telescope concatenation), and the pseudo CwF-morphism $(\blank)_\cred{1} : \bTel^\cred{2} \to \bTel$.
Moreover, in this case the latter is actually a strict CwF-morphism, because telescope concatenation is strictly associative.

\begin{definition}\label{def:tel-disp}
Let $\C : \M\coop\to\Cat$ be a dTT natural model with telescopes.
We say $\C$ \textbf{has telescope display} if it is equipped with
\begin{enumerate}
\item An internal pseudo CwF morphism that preserves substitution, the empty context, and $\Sigma$-types strictly:
\[ (\blank)\d : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm^\cred{2} \]
\item An equality between the composite $(\lock_\trisq)^*\bTel_\sm \xrightarrow{(\blank)\d} \bTel_\sm^\cred{2} \xrightarrow{(\blank)_\cred{0}} \bTel_\sm$ and the key transformation $(\blank)\sqbkt{\key^{\trisq\le \id_\sm}} : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm$.
Since the latter is a strict morphism, that means that so is the former.
\item A strict internal CwF morphism
\[(\blank)\D : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm \]
and an isomorphism of pseudo CwF morphisms between $(\blank)\D$ and the composite morphism $(\lock_\trisq)^*\bTel_\sm \xrightarrow{(\blank)\d} \bTel_\sm^\cred{2} \xrightarrow{(\blank)_\cred{1}} \bTel$, that is the identity on underlying functors.
\end{enumerate}
\end{definition}

We have not assumed \textit{a priori} in \cref{def:tel-disp} that $\C$ has d\'ecalage, but it is actually included: the morphism $(\blank)\D$ is of course the same as in \cref{def:decalage}, and the transformation $\evens : \Theta\D \to \Theta$ from \cref{def:decalage} arises in \cref{def:tel-disp} as the image of $\Theta$ under the underlying functor of $(\blank)\d$.
The additional data in \cref{def:tel-disp} beyond this is the $1$-part of the action of $(\blank)\d$ (the $\cred{0}$-part is determined by the composition with $(\blank)_\cred{0}$ equaling $(\blank)\sqbkt{\key^{\trisq\le \id_\sm}}$) making it a pseudo CwF morphism preserving substitution and $\Sigma$-types strictly, and the isomorphism on \emph{`types'} (dependent telescopes) between $(\blank)\D$ and the composite of $(\blank)\d$ with $(\blank)_\cred{1}$.
But since the latter is to be a pseudo CwF transformation (see~\cite[Appendix B]{ccd:undeceq-flccc}), and since $(\blank)\D$ is strict and the underlying functor is the identity this just means that this isomorphism must coincide with the $\cred{1}$-part of the comprehension coherence isomorphism of $(\blank)\d$ (the $\cred{0}$-part being the identity).

So all that remains is the $\cred{1}$-part of the action of $(\blank)\d$ on meta-abstracted telescopes, preserving substitution and telescope concatenation, and coherence isomorphisms relating it to comprehension.
This gives the rules of \cref{sec:meta-abstr-displ}, which have \cref{sec:teldisp} as a special case.
In particular, since the $\cred{1}$-part of the comprehension of $(\Upsilon, \Upsilon\d)$ in $\bTel^\cred{2}$ is $(\Upsilon\ext\Upsilon\d)$, the comprehension isomorphisms are the pairing $\pair{\blank}{\blank}$ together with $\ev$ and $\od$.

Finally, we consider display of types, as in \cref{sec:displ-meta-abstr}, and its relation to d\'ecalage as in \cref{sec:comp-tel-dec,sec:comp-metaabsdec}.
In some ways this is simpler, since we don't have to worry about rearranging between display and d\'ecalage; but in other ways it is more complicated, since we have to take account of extending dependent telescopes by types.

To start with, note that the internal telescope model $\bTel$ of any CwF has a \emph{`sub-model'} $\bTel_\cred{1}$ whose internal category of \emph{`contexts'} is the same (telescopes), but whose internal presheaf of \emph{`types'} consists of the \emph{length-$\cred{1}$ telescopes}, i.e.\ single types annotated by a modality.
% We can then construct $\bTel_1^2$ as before, whose \emph{`contexts'} are maps of telescopes $\theta_{01} : \Theta_1 \to \Theta_0$ as before, but whose \emph{`types'} are pairs of types $A_0 \in \Ty(\Gamma\ext \Theta_0\ce\lock_\mu)$ with $A_1\in \Ty(\Gamma \ext \Theta_1 \ce (x:^\mu A_0\sqbkt{\theta_{01}}))$.
Note that unlike $\bTel$, it does not automatically have $\Sigma$-types.

\begin{definition}\label{def:ty-disp}
Let $\C : \M\coop\to\Cat$ be a dTT natural model with telescopes.
We say $\C$ \textbf{has type display} if it is equipped with
\begin{enumerate}
\item An internal strict CwF morphism:
\[ (\blank)\d : (\lock_\trisq)^*\bTel_{\sm,\cred{1}} \to \bTel_\sm^\cred{2} \]
\item An equality between the composite $(\lock_\trisq)^*\bTel_\sm \xrightarrow{(\blank)\d} \bTel_\sm^\cred{2} \xrightarrow{(\blank)_\cred{0}} \bTel_\sm$ and the key transformation $(\blank)\sqbkt{\key^{\trisq\le \id_\sm}} : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm$.
\item If a length-1 telescope $\A$ is non-modal, then the telescope $\A\d$ is a single non-modal type.\label{item:l1tnm}
\item If a length-1 telescope $\A$ is nontrivially modal, then the telescope $\A\d$ is empty.\label{item:l1tm}
\end{enumerate}
\end{definition}

Note that, like \cref{def:tel-disp}, this definition includes d\'ecalage.
It represents the rules for display from \cref{sec:disp-ty,sec:displ-meta-abstr}, and the rules for computing d\'ecalage on a telescope extended by a type from \cref{sec:comp-tel-dec}.
Of course, with both telescope display and type display we want them to be compatible.

\begin{definition}
Let $\C : \M\coop\to\Cat$ be a dTT natural model with telescope display.
We say it has \textbf{complete display} if the restriction of
$(\blank)\d : (\lock_\trisq)^*\bTel_\sm \to \bTel_\sm^\cred{2}$ to $(\lock_\trisq)^*\bTel_{\sm,\cred{1}}$ is an internal strict CwF morphism such that
\begin{itemize}
\item \Cref{item:l1tnm,item:l1tm} of \cref{def:ty-disp} hold.
\item The rules in \cref{sec:comp-metaabsdec} for computing meta-abstracted d\'ecalage in terms of type display hold.
\item The rules in \cref{sec:comp-matd} for computing meta-abstracted telescope display in terms of type display hold.
\end{itemize}
\end{definition}

Finally, we add the compatibility conditions with type-formers:

\begin{definition}
Let $\C : \M\coop\to\Cat$ be a dTT natural model with telescopes, d\'ecalage, telescope display, and type display.
We say that \textbf{display respects $\Pi$-types} (respectively \textbf{universes}) if the rules in \cref{sec:comp-telesc-displ} hold.
\end{definition}

This completes the description of the abstract categorical semantics of the theory of \cref{sec:syntax}: it is a dTT natural model with telescopes and complete display that respects $\Pi$-types and universes.
However, as noted in \cref{sec:syntax}, when telescopes are lists of types, as they almost always are, much of this structure can be deduced from the rest.

\begin{theorem}
Let $\C$ be a dTT natural model, with telescopes defined from types as in \cref{thm:sctx-as-lists}, and with type display defined relative to these telescopes.
Then there is a unique way to extend this type display on $\C$ to complete display.
\end{theorem}
\begin{proof}
The rules in \cref{sec:dtel} for computing telescope display and d\'ecalage in terms of type display uniquely determine those operations when telescopes are defined as lists of types.
\end{proof}

Using this, we can verify that our intended model is indeed a model.

\begin{theorem}\label{thm:sm-has-disp}
The simplicial model of \cref{sec:simplicial-model,sec:modal-semantics} has type display, and hence complete display, which respects $\Pi$-types and universes.
\end{theorem}
\begin{proof}
We constructed a display operation for the simplicial model in \cref{sec:simplicial-model}, but it does not yet have exactly the needed form.
What we have so far is a \emph{`global'} operation that d\'ecalages the whole context:
\[ \infer{\gamma : \Gamma \vdash_{\sm} \A~\gamma \type}
{\gamma^\cblu{+} : \Gamma\D, ~\a : \A^{\rho_\Gamma} ~\gamma^\cblu{+} \vdash_{\sm} \A\d ~\gamma^\cblu{+}~\a \type}.
\]
(Note that this is only defined on the original simplicial model $\sm$, not the extended one $\sm_+$: indeed, d\'ecalage is not even defined on flat contexts.)
But the (meta-abstracted version of the) operation we specified in the syntax of \cref{sec:syntax} is a \emph{`local'} one that only d\'ecalages part of the context, keeping the rest of it modally locked away:
\[  \infer{\gamma:\Gamma,~\lock_\trisq,~\upsilon:\Upsilon \vdash_\sm \A~\gamma~\upsilon \type}{
\gamma:\Gamma,~\upsilon^\cblu{+}:\Upsilon\D,~\a:\A^{\key^{\trisq\le \id_\sm}}~\gamma~(\upsilon^\cblu{+})\ev \vdash_\sm \A\d~\gamma~\upsilon^\cblu{+}~\a \type}
\]
However, it is straightforward to obtain the latter from the former.
In $\sm_+$, a context of the form $\bkt{\gamma:\Gamma,~\lock_\trisq,~\upsilon:\Upsilon}$ is not flat, hence lies essentially in $\sm$ so that d\'ecalage is defined on it.
Furthermore, we already observed that $\bkt{\Gamma,~\lock_\sq}\D \equiv \bkt{\Gamma,~\lock_\sq}$ since $\lock_\sq$ lands in constant presheaves.
Thus, when $\Upsilon$ is a telescope built out of types, we have
\[\bkt{\gamma:\Gamma,~\lock_\trisq,~\upsilon:\Upsilon}\D
\equiv \bkt{\gamma:\Gamma,~\lock_\trisq,~\upsilon^\cblu{+}:\Upsilon\D}
\]
and so the global operation yields as a special case
\[ \infer{\gamma:\Gamma,~\lock_\trisq,~\upsilon:\Upsilon \vdash_{\sm_+} \A~\gamma~\upsilon \type}
{\gamma:\Gamma,~\lock_\trisq,~\upsilon^\cblu{+}:\Upsilon\D,~\a : \A^{\rho} ~\gamma~\upsilon^{\cblu{+}} \vdash_{\sm_+} \A\d~\gamma~\upsilon^\cblu{+}~\a \type}.
\]
Now we simply substitute along $\key^{\trisq\le \id_\sm}$ to obtain the desired local rule.
The necessary computation rules for d\'ecalage, $\Pi$-types, and universes follow immediately from the rules we proved for the global operation in \cref{sec:simplicial-model}.
\end{proof}

\subsubsection{Display of $\oldomega$-limits}
\label{sec:displim}

Finally, when we have both display and also $\oldomega$-limits, it is reasonable to require the former to compute on the latter, in the following way.
Suppose that $\Gamma,\lock_{\trisq} \ext \phi:\Phi \vdash \cblu{\widetilde{\Upsilon}}~\phi \inftel$, and we want to compute $\Gamma,~\phi:\Phi\D,~\mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}} \vdash \lim~\cblu{\widetilde{\Upsilon}}\d~\phi~\mathfrak{\cblu{u}}$.
Then by definition, we have
\begin{align*}
\Gamma,\lock_{\trisq} &\vdash \cblu{\Upsilon}^{\cred{\partial}\n} \slfrac{\tel}{_{\phi:\Phi}}
\\
\Gamma,\lock_{\trisq} &\vdash \cblu{\Upsilon}^{\n} \slfrac{\type}{_{\phi:\Phi,\;\cblu{\partial}\upsilon:\cblu{\Upsilon}^{\cred{\partial}\n}~\phi}}
\end{align*}
and therefore
\begin{align*}
\Gamma &\vdash (\cblu{\Upsilon}^{\cred{\partial}\n})\d \slfrac{\tel}{_{\phi:\Phi\D,\;\cblu{\partial}\upsilon : \cblu{\Upsilon}^{\cred{\partial}\n}\,\phi\ev}}
\\
\Gamma &\vdash (\cblu{\Upsilon}^{\n})\d \slfrac{\type}{_{\phi:\Phi\D,\;\cblu{\partial}\upsilon:(\cblu{\Upsilon}^{\cred{\partial}\n})\D\,\phi,\;\upsilon : \cblu{\Upsilon}^{\n}\,\phi\ev\,\cblu{\partial}\upsilon\ev}}
\end{align*}
Weakening and substituting to the needed context $\Gamma,~\phi:\Phi\D,~\mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}$, we have
\begin{align*}
\Gamma,~\phi:\Phi\D,~\mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}
&\vdash (\cblu{\Upsilon}^{\cred{\partial}\n})\d~\phi~(\res^{\cred{\partial}\n}~\mathfrak{\cblu{u}}) \tel
\\
\Gamma,~\phi:\Phi\D,~\mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}, ~ \cblu{\partial}\upsilon : (\cblu{\Upsilon}^{\cred{\partial}\n})\d~\phi~(\res^{\cred{\partial}\n}~\mathfrak{\cblu{u}})
&\vdash (\cblu{\Upsilon}^{\n})\d~\phi~\pair{\res^{\cred{\partial}\n}~\mathfrak{\cblu{u}}}{\cblu{\partial}\upsilon}~(\res^{\n}~\mathfrak{\cblu{u}}) \type
\end{align*}
such that
\begin{align*}
\bkt{\cblu{\partial}\upsilon : \cblu{\widetilde{\Upsilon}}^{\cred{\partial}\n}, \upsilon : \cblu{\widetilde{\Upsilon}}^\n~\cblu{\partial}\upsilon}
\d~\phi~\sqbkt{\res^{\cred{\partial}\n}~\cblu{\mathfrak{\cblu{u}}}, ~\res^\n~\cblu{\mathfrak{\cblu{u}}}}\\
&\equiv \bkt{\cblu{\partial}\upsilon : (\cblu{\widetilde{\Upsilon}}^{\cred{\partial}\n})\d~\phi~(\res^{\cred{\partial}\n}~\cblu{\mathfrak{\cblu{u}}}),~
\upsilon : (\cblu{\widetilde{\Upsilon}}^\n)\d~\phi~\pair{\res^{\cred{\partial}\n}~\cblu{\mathfrak{\cblu{u}}}}{\cblu{\partial}\upsilon}~(\res^\n~\cblu{\mathfrak{\cblu{u}}})}.
\end{align*}
Thus, these data form another infinite telescope, which we denote
\begin{align*}
\Gamma,~\phi:\Phi\D,~\mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}
&\vdash \widetilde{\Upsilon}\d~\phi~\mathfrak{\cblu{u}} \inftel\\
\end{align*}
We say that \textbf{display respects $\oldomega$-limits} if
\begin{align*}
\Gamma,~\phi:\Phi\D, ~ \mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}
\lim~\cblu{\widetilde{\Upsilon}}\d~\phi~\mathfrak{\cblu{u}} \equiv
\lim(\widetilde{\Upsilon}\d~\phi~\mathfrak{\cblu{u}})\\
\Gamma,~\phi:\Phi\D, ~ \mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}
&\vdash (\res^{\cred{\partial}\n})\d~\phi~\mathfrak{\cblu{u}} \equiv \res^{\cred{\partial}\n}~\phi~\mathfrak{\cblu{u}}\\
\Gamma,~\phi:\Phi\D, ~ \mathfrak{\cblu{u}}:\lim~\cblu{\widetilde{\Upsilon}}
&\vdash (\res^{\n})\d~\phi~\mathfrak{\cblu{u}} \equiv \res^{\n}~\phi~\mathfrak{\cblu{u}}.
\end{align*}
where in the last two equations, the left-hand side is a restriction relative to $\widetilde{\Upsilon}$, and on the right-hand side it is relative to $\widetilde{\Upsilon}\d$.

\begin{theorem}
Display respects $\oldomega$-limits in the simplicial model.
\end{theorem}
\begin{proof}
This holds essentially by construction of $\oldomega$-limits therein, plus passing across the translation between different forms of display from \cref{thm:sm-has-disp}.
\end{proof}

\subsection{Semantics of semi-simplicial types}
\label{sec:sem-sst}

Finally, we describe semantics for the display coinductive types of \cref{sec:dcoind}, in particular including $\SST$.
As with most kinds of coinductive definitions, they are terminal coalgebras of some sort, but in this case they are terminal coalgebras for a \emph{copointed} endofunctor.

\subsubsection{Terminal coalgebras for copointed endofunctors}
\label{sec:term-coalg}

\begin{definition}
A \textbf{copointed endofunctor} of a category $\MC$ is a functor $\F:\MC\to \MC$ together with a natural transformation $\epsilon : \F \to \id_\MC$.
A \textbf{coalgebra} for a copointed endofunctor is an object $\X$ with a morphism $\x : \X\to \F\X$ such that the composite $\X \xrightarrow{\x} \F\X \xrightarrow{\epsilon_\X} \X$ is the identity.
A \textbf{terminal coalgebra} is a terminal object of the category of coalgebras.
\end{definition}

As usual, we can obtain terminal coalgebras by a sequential limit construction.
However, in the copointed case it does not suffice to simply consider the limit of the tower $\cdots \to \F^\cred{3}\One \to \F^\cred{2}\One \to \F\One \to \One$; we have to incorporate the transformation $\epsilon$ in some way.
The classical way to do this (e.g.\ the dual of~[16]) is to take \emph{equalisers} at each step.
However, equalisers are difficult to understand homotopy-theoretically, so we replace them by a pullback.
The following definition is a partial dual of~\cite[Definition 8.6]{shulman:univinj}.

\begin{definition}
Given a natural transformation $\epsilon : \F \to \G$ and a morphism $\f :\X\to \Y$ in the domain of $\F$ and $\G$, we write $\leibhom\epsilon \f$ for the gap map in the following pullback, assuming that the pullback exists.
\[
\begin{tikzcd}
\F\X \ar[dr,dotted,"\leibhom{\epsilon}{\f}" ] \ar[drr,bend left,"\F\f"] \ar[ddr,bend right,"\epsilon_\X"'] \\
& \F\Y \times_{\G\Y} \G\X \ar[r] \ar[d] \drpullback & \F\Y \ar[d,"\epsilon_\Y"] \\
& \G\X \ar[r,"\G\f"'] & \G\Y
\end{tikzcd}
\]
If the domain and codomain of $F$ and $G$ have a notion of \emph{`fibration'}, we say that $\epsilon$ is a \textbf{Quillen pre-fibration} if whenever $\f$ is a fibration, so is $\leibhom{\epsilon}{\f}$.
\end{definition}

For example, we have:

\begin{lemma}\label{thm:evens-qpf}
In a category of telescopes, consider the fibrations to be the morphisms isomorphic to a dependent projection of some telescope.
Then the transformation $\evens : (\blank)\D \to (\blank)\sqbkt{\key^{\trisq\le \id_\sm}}$ from \cref{def:decalage} is a Quillen pre-fibration.
\end{lemma}
\begin{proof}
Given a dependent projection $(\Theta\ext\Upsilon) \to \Theta$ in $\Telover(\Gamma\ce\lock_\trisq)$, the gap map is isomorphic to the dependent projection of $\Upsilon\d$:
\[ (\Theta\D\ext \Upsilon\sqbkt{\key^{\trisq\le 1}} \ext \Upsilon\d) \to (\Theta\D\ext \Upsilon\sqbkt{\key^{\trisq\le 1}}).\qedhere \]
\end{proof}

\begin{theorem}\label{thm:termcoalg}
Suppose $\MC$ is a category with a terminal object and a notion of fibration that is stable under pullback, and that $\F$ is a copointed endofunctor of $\MC$ such that $\epsilon :\F\to \id_\MC$ is a Quillen pre-fibration.
Suppose also that $\MC$ has limits of inverse $\omega$-sequences of fibrations, and that $\F$ preserves these limits.
Then there is a terminal $\F$-coalgebra.
\end{theorem}
\begin{proof}
We define inductively a sequence of objects $\X_\n$ with morphisms $\x_{\n+\cred{1}} : \X_{\n+\cred{1}} \to \F \X_{\n}$ and $\g_{\n+\cred{1}}: \X_{\n+\cred{1}} \to \X_\n$ such that $\F\g_\n \circ \x_{\n+\cred{1}} = \x_\n \circ \g_{\n+\cred{1}}$ and $\epsilon_{\X_\n} \circ \x_{\n+\cred{1}} = \g_{\n+\cred{1}}$, and each $\g_\n$ is a fibration.

Let $\X_\cred{0}=\One$, the terminal object, and let $\X_\cred{1} = \F \X_\cred{0} = \F \One$.
For $\n>\cred{0}$, let $\g_\n$ be the fibration $\X_{\n} \xrightarrow{\x_{\n}} \F \X_{\n-\cred{1}}\xrightarrow{\epsilon_{\X_{\n-\cred{1}}}}\X_{\n-\cred{1}}$ as above, and define $\X_{\n+\cred{1}}$ by the following pullback:
\begin{equation}
\label{eq:xnplusone}
\begin{tikzcd}
\X_{\n+\cred{1}} \ar[r,"\x_{\n+\cred{1}}"] \ar[d,"\g_{\n+\cred{1}}"'] \drpullback & \F \X_\n \ar[d,"\leibhom{\epsilon}{\g_\n}"]\\
\X_\n \ar[r,"{(\id,\x_\n)}"'] & \X_\n \times_{\X_{\n-\cred{1}}} \F \X_{\n-\cred{1}}.
\end{tikzcd}
\end{equation}
The commutativity of this square says that $\F\g_\n \circ \x_{\n+\cred{1}} = \x_\n \circ \g_{\n+\cred{1}}$ and $\epsilon_{\X_\n} \circ \x_{\n+\cred{1}} = \g_{\n+\cred{1}}$.
And by assumption, $\leibhom{\epsilon}{\g_\n}$ is a fibration, hence so is its pullback $\g_{\n+\cred{1}}$.

Now let $\X_\cred{\infty}$ be the limit of the $\omega$-sequence of fibrations
\[ \X_\cred{\infty} \cdots \xrightarrow{\g_{\n+\cred{1}}} \X_\n \xrightarrow{\g_\n} \cdots \xrightarrow{\g_\cred{2}} \X_\cred{1} \xrightarrow{\g_\cred{1}}\X_\cred{0} = \One.\]
Since $\F$ preserves limits of inverse $\omega$-sequences, $\F \X_\cred{\infty}$ is the limit of the corresponding sequence
\[ \F\X_\infty \cdots \xrightarrow{\F \g_{\n+\cred{1}}} \F\X_\n \xrightarrow{\F \g_\n} \cdots \xrightarrow{\F \g_\cred{2}} \F \X_\cred{1} \xrightarrow{\F \g_\cred{1}} \F \X_\cred{0} = \One.\]
The morphisms $\x_\n$ and $\epsilon_{\X_\n}$ form fence diagrams:
\[
\begin{tikzcd}
\X_\cred{\infty}  \ar[d,"\x_\cred{\infty}"'] \ar[r] & \cdots \ar[r] &
\X_\cred{3} \ar[r,"\g_\cred{3}"'] \ar[dr,"\x_\cred{3}"'] &
\X_\cred{2} \ar[r,"\g_\cred{2}"'] \ar[dr,"\x_\cred{2}"'] &
\X_\cred{1} \ar[r,"\g_\cred{1}"'] \ar[dr,"\x_\cred{1}"'] &
\X_\cred{0}\\
\F \X_\cred{\infty} \ar[d,"\epsilon_{\X_\cred{\infty}}"'] \ar[r] & \cdots \ar[r] &
\F\X_\cred{3} \ar[r,"\F\g_\cred{3}"'] \ar[d,"\epsilon_{\X_\cred{3}}"] &
\F\X_\cred{2} \ar[r,"\F\g_\cred{2}"'] \ar[d,"\epsilon_{\X_\cred{2}}"] &
\F\X_\cred{1} \ar[r,"\F\g_\cred{1}"'] \ar[d,"\epsilon_{\X_\cred{1}}"] &
\F\X_\cred{0} \ar[d,"\epsilon_{\X_\cred{0}}"] \\
\X_\cred{\infty} \ar[r] & \cdots \ar[r] &
\X_\cred{3} \ar[r,"\g_\cred{3}"'] &
\X_\cred{2} \ar[r,"\g_\cred{2}"'] &
\X_1 \ar[r,"\g_\cred{1}"'] &
\X_\cred{0}
\end{tikzcd}
\]
composed of the parallelograms $\F\g_\n \circ \x_{\n+\cred{1}} = \x_\n \circ \g_{\n+\cred{1}}$ from our construction, and naturality squares $\epsilon_{\X_\n} \circ \F \g_{\n+\cred{1}} = \g_{\n+\cred{1}} \circ \epsilon_{\X_{\n+\cred{1}}}$.
The former induces a map of limits $\x_\cred{\infty} : \X_\cred{\infty} \to \F \X_\cred{\infty}$, while by naturality the latter induces $\epsilon_{\X_\cred{\infty}}$.
The universal property of limits implies that $\epsilon_{\X_\cred{\infty}}\circ \x_\cred{\infty}$ is induced by the composite fence, and since $\g_{\n+\cred{1}} = \epsilon_{\X_\n}\circ \x_{\n+\cred{1}}$ this is
\[
\begin{tikzcd}
\X_\cred{\infty}  \ar[d,"\id_{\X_\cred{\infty}}"'] \ar[r] & \cdots \ar[r] &
\X_\cred{3} \ar[r,"\g_\cred{3}"'] \ar[dr,"\g_\cred{3}"'] &
\X_\cred{2} \ar[r,"\g_\cred{2}"'] \ar[dr,"\g_\cred{2}"'] &
\X_\cred{1} \ar[r,"\g_\cred{1}"'] \ar[dr,"\g_\cred{1}"'] &
\X_\cred{0}\\
\X_\cred{\infty} \ar[r] & \cdots \ar[r] &
\X_\cred{3} \ar[r,"\g_\cred{3}"'] &
\X_\cred{2} \ar[r,"\g_\cred{2}"'] &
\X_\cred{1} \ar[r,"\g_\cred{1}"'] &
\X_\cred{0}
\end{tikzcd}
\]
which induces the identity $\id_{\X_\cred{\infty}}$.
Thus, $\X_\cred{\infty}$ is an $\F$-coalgebra.

Now suppose $\y:\Y \to \F\Y$ is another $\F$-coalgebra.
We construct inductively maps $\h_\n : \Y \to \X_\n$ such that $\x_{\n+\cred{1}} \circ \h_{\n+\cred{1}} = \F \h_\n \circ \y$ and $\g_{\n+\cred{1}}\circ \h_{\n+\cred{1}} = \h_\n$.
We start with $\h_\cred{0} : \Y \to \X_\cred{0} = \One$ the unique morphism, and $\h_\cred{1} : \Y \to \X_\cred{1} = \F\X_\cred{0}$ the composite $\Y \xrightarrow{\y} \F\Y \xrightarrow{\F\h_\cred{0}} \F\X_\cred{0}$.
Then we induce $\h_{\n+\cred{1}}$ by the universal property of the pullback defining $\X_{\n+\cred{1}}$:
\[
\begin{tikzcd}
\Y \ar[ddr,bend right,"\h_\n"'] \ar[drr,bend left,"\F\h_\n\circ \y"] \ar[dr,dashed,"\h_{\n+\cred{1}}"] \\
&\X_{\n+\cred{1}} \ar[r,"\x_{\n+\cred{1}}"] \ar[d,"\g_{\n+\cred{1}}"] \drpullback & \F \X_\n \ar[d,"\leibhom{\epsilon}{\g_\n}"]\\
&\X_\n \ar[r,"{\bkt{\id,\;\x_\n}}"'] & \X_\n \times_{\X_{\n-\cred{1}}} \F \X_{\n-\cred{1}}.
\end{tikzcd}
\]
This is valid because using the inductive assumptions about $\h_\n$ and $\h_{\n-\cred{1}}$, we have
\begin{align*}
\epsilon_{\X_\n} \circ \F \h_\n \circ \y
&= \h_\n \circ \epsilon_{\Y} \circ \y\\
&= \h_\n
\end{align*}
\begin{align*}
\F\g_{\n} \circ \F\h_\n \circ \y
&= \F\bkt{\g_\n \circ \h_\n} \circ \y\\
&= \F\h_{\n-\cred{1}} \circ \y\\
&= \x_\n \circ \h_\n,
\end{align*}
and the two triangles relating to $\h_{\n+\cred{1}}$ show that it has the necessary properties.

Now, the equations $\g_{\n+\cred{1}}\circ \h_{\n+\cred{1}} = \h_\n$ imply there is an induced map $\h_\cred{\infty} : \Y \to \X_\cred{\infty}$, such that $\x_\cred{\infty} \circ \h_\cred{\infty}$ is induced by the composites $\x_{\n+\cred{1}}\circ \h_{\n+\cred{1}}$.
But $\x_{\n+\cred{1}} \circ \h_{\n+\cred{1}} = \F \h_\n \circ \y$, and the morphisms $\F \h_\n$ induce the limit map $\F \h_\cred{\infty}$.
Thus, $\h_\cred{\infty}$ is an $\F$-coalgebra morphism.

Finally, suppose $\k:\Y\to \X_\cred{\infty}$ is any $\F$-coalgebra morphism, so we have $\x_\cred{\infty} \circ \k = \F \k \circ \y$.
Then $\k$ is uniquely determined by the maps $\k_\n : \Y \to \X_\n$, and we have $\x_{\n+\cred{1}} \circ \k_{\n+\cred{1}} = \F \k_\n \circ \y$.
But this equation implies by induction that $\k_\n = \h_\n$ for all $\n$, hence $\k = \h_\cred{\infty}$.
\end{proof}

\subsubsection{Display coinductive types}
\label{sec:displ-coind-types}

Let $\MC$ be a dTT natural model with telescopes, d\'ecalage, telescope display, type display respecting $\Pi$-types and universes, and $\Pi$-telescopes.
We will apply \cref{thm:termcoalg} in $\Telover(\Gamma\ce\lock_\trisq\ext \Phi)$, in which the fibrations are the morphisms isomorphic to the dependent projection from some telescope,
\[(\Gamma\ce\lock_\trisq\ext \Phi\ext \Theta\ext \Upsilon) \to (\Gamma\ce\lock_\trisq\ext \Phi\ext\Theta).\]
Suppose given the input data for a display coinductive type, consisting of
\begin{mathpar}
\Gamma\in \MC
\and
\Phi\in\Tel(\Gamma\ce\lock_\trisq)
\and
\A \in \Ty(\Gamma\ce\lock_\trisq\ext\Phi)
\and
\B \in \Tel(\Gamma\ce\lock_\trisq\ext\Phi\ce\A)
\and
\sigma\in \PSub\left((\Gamma\ce\lock_\trisq\ext\Phi\ce\A\ext \B),~ \Phi\d\right).
\end{mathpar}
Categorically, this yields the data of a sort of \emph{`display polynomial'}, where we indicate fibrations with $\twoheadrightarrow$:
\[
\begin{tikzcd}
(\Gamma\ce\lock_\trisq\ext\Phi\D) \ar[d,->>] &
(\Gamma\ce\lock_\trisq\ext\Phi\ce \A\ext \B) \ar[r,->>,"\pi"] \ar[dl,->>,"\tau\pi"'] \ar[l,"\sigma"'] &
(\Gamma\ce\lock_\trisq\ext\Phi\ce \A) \ar[dr,->>,"\tau"] \\
(\Gamma\ce\lock_\trisq\ext\Phi) \ar[rrr,equals] &&& (\Gamma\ce\lock_\trisq\ext\Phi)
\end{tikzcd}
\]
The left vertical map is a fibration because it is isomorphic to the dependent projection
\[ (\Gamma\ce\lock_\trisq\ext\Phi\ext\Phi\d) \to (\Gamma\ce\lock_\trisq\ext\Phi). \]
Since everything is in the category of telescopes over $\Gamma\ce\lock_\trisq$, we will omit it from the notation for conciseness, so that the above display polynomial becomes
\[
\begin{tikzcd}
\Phi\D \ar[d,->>] &
(\Phi\ce \A\ext \B) \ar[r,->>,"\pi"] \ar[dl,->>,"\tau\pi"'] \ar[l,"\sigma"'] &
(\Phi\ce \A) \ar[dr,->>,"\tau"] \\
\Phi \ar[rrr,equals] &&& \Phi
\end{tikzcd}
\]

This display polynomial then defines a copointed endofunctor of $\Telover(\Gamma\ce\lock_\trisq\ext\Phi)$ as follows:
\begin{mathpar}
\infer{\Gamma,~\lock_\trisq \vdash \X \slfrac{\tel}{_{\phi:\Phi}}}{\Gamma,~\lock_\trisq\vdash \F\X \slfrac{\tel}{_{\phi\;:\;\Phi,~ \x\;:\;\X~\phi}}}
\and
\F\X \equiv \dbkt{ \a:\A~\phi,~ \xp : (\b:\B~\phi~\a) \to \X\d~\pair{\phi}{\sigma~\a~\b}~\x }_{\;\phi\;:\;\Phi,~\x\;:\;\X\phi}
\end{mathpar}
Here the $\to$ denotes a $\Pi$-telescope (\cref{sec:pi-telescopes}), and $\X\d$ denotes meta-abstracted telescope display (\cref{sec:meta-abstr-displ}); this is why we wanted those in the syntax.
Note that $\F\X$ is meta-abstracted over $\Phi$ extended by $\X$, so it lies in $\Telover(\Gamma\ce\lock_\trisq\ext\Phi\ext \X)$ rather than $\Telover(\Gamma\ce\lock_\trisq\ext\Phi)$.
The actual \emph{endo}functor of $\Telover(\Gamma\ce\lock_\trisq\ext\Phi)$ is thus $\Ftil(\X) \equiv (\X \ext \F\X)$.
The weakening projection $(\X\ext \F\X) \to \X$ is then a copointing $\epsilon : \Ftil \to \id$ of this endofunctor, which is evidently a fibration.
More than this, we have:

\begin{lemma}
The copointing $\epsilon : \Ftil \to \id$ is a Quillen pre-fibration.
\end{lemma}
\begin{proof}
Suppose given a fibration over $\X$, meaning a dependent telescope
\[\Gamma,~\lock_\trisq \vdash \Y \slfrac{\tel}{_{\phi\;:\;\Phi,~\x\;:\;\X~\phi}}.\]
Then we have
\[\Gamma,~\lock_\trisq \vdash \dbkt{\x\;:\;\X~\phi\ext \y\;:\;\Y~\phi~\x}_{\;\phi\;:\;\Phi} \slfrac{\tel}{_{\phi\;:\;\Phi}} \]
which we write as $\X\Y$ for conciseness.
Then by definition, we have
\begin{equation*}
% F\left(\dbkt{(x:X~\phi\ext y:Y~\phi~x)}_{\phi:\Phi}\right)\\
\F(\X\Y)
\equiv
\dbkt{ \a:\A~\phi,~ \z\cblu{'} : (\b:\B~\phi~\a) \to (\X\Y)\d~\pair{\phi}{\sigma~\a~\b}~\sqbkt{\x\ext \y} }_{\;\phi\;:\;\Phi,~\x\;:\;\X~\phi,~\y\;:\;\Y~\phi~\x}.
\end{equation*}
To simplify this, note that by the rules in \cref{sec:meta-abstr-displ}
\begin{equation*}
(\X\Y)\d~\pair{\phi}{\sigma~\a~\b}~\sqbkt{\x\ext \y}
\equiv \left(\x\cblu{'}:\X\d~\pair{\phi}{\sigma~\a~\b}~\x \ext \Y\d~\pair{\phi}{\sigma~\a~\b}~\pair{\x}{\cblu{x'}}~\y\right)
\end{equation*}
and therefore by the rules in \cref{sec:pi-telescopes}
\begin{multline*}
(\b:\B~\phi~\a) \to (\X\Y)\d~\pair{\phi}{\sigma~\a~\b}~\sqbkt{\x\ext \y}\\
\equiv
\left(\delta: (\b:\B~\phi~\a) \to \X\d~\pair{\phi}{\sigma~\a~\b}~\x ~\ext~
\epsilon : (\b:\B~\phi~\a) \to \Y\d~\pair{\phi}{\sigma~\a~\b}~\pair{\x}{\delta~\b}~\y\right).
\end{multline*}
Now when $\delta$ is paired with $\a:\A~\phi$, it yields $\F\X$.
Thus, the relevant gap map
\[
\begin{tikzcd}
\X\Y \ext \F(\X\Y) \ar[dr,dashed] \ar[drr,bend left] \ar[ddr,bend right] \\
& \X\Y\ext \F(\X) \ar[r] \ar[d] \drpullback & \X\ext \F(\X) \ar[d] \\
& \X\Y \ar[r] & \X
\end{tikzcd}
\]
is the dependent projection from the telescope
\begin{multline}\label{eq:fgap}
\dbkt{(\b:\B\;\phi\;\a) \to \Y\d\;\pair{\phi}{\sigma\;\a\;\b}\;\pair{\x}{\delta\;\b}\;\y}_{\;\phi\;:\;\Phi,\;\x\;:\;\X\;\phi,\;\y\;:\;\Y\;\phi \;\x,\;\a\;:\;\A\;\phi,}\\_{\delta\;:\;(\b\;:\;\B\;\phi\;\a) \to \X\d\; \pair{\phi}{\sigma\;\a\;\b}\;\x}
\end{multline}
and thus a fibration.
\end{proof}

\begin{lemma}
The endofunctor $\Ftil$ preserves inverse limits of $\omega$-sequences of fibrations.
\end{lemma}
\begin{proof}[Sketch of proof]
This follows from the $\eta$-rules for inverse limits, together with the fact that display also preserves inverse limits.
\end{proof}

Therefore, by \cref{thm:termcoalg}, there exists a terminal $\Ftil$-coalgebra.
Moreover, since we have assumed that inverse limits are representable by single types, this coalgebra is a type and not just a telescope.
This type is our candidate for the display coinductive type; we can unpack its definition as follows.
The construction produces a tower of fibrations $g_n$, which is to say a sequence of finite telescopes dependent on the previous ones:
\begin{align*}
\phi:\Phi &\vdash \X^{\cred{\partial}\n}~\phi \tel \\
\phi:\Phi , ~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi &\vdash \X^\n~\phi~\cblu{\partial}\x \tel\\
\phi:\Phi &\vdash \X^{\cred{\partial}(\n+\cred{1})}~\phi \equiv (\cblu{\partial}\x:\X^{\cred{\partial}\n}~\phi ,~ \x : \X^\n~\phi~\cblu{\partial}\x)
\end{align*}
The object $\X_{\n+\cred{1}}$ in \cref{sec:term-coalg} corresponds to the telescope
\[(\phi:\Phi,~\cblu{\partial}\x: \X^{\cred{\partial} (\n+\cred{1})}~\phi ) = (\phi:\Phi,~\cblu{\partial}\x: \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x ).\]
Each morphism $\x_{\n+\cred{1}} : \X_{\n+\cred{1}} \to \Ftil \X_{\n}$ such that $\epsilon \circ \x_{\n+\cred{1}} = \g_{\n+\cred{1}}$ then corresponds to a term
\[ \phi:\Phi,~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x \vdash \xi_\n : \F (\X^{\cred{\partial}\n})~\phi~\cblu{\partial}\x.
\]
By definition of $\F$, $\xi_n$ is equivalent to two terms
\begin{align*}
\phi:\Phi,~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x
&\vdash \h_\n~\phi~\cblu{\partial}\x~\x : \A~\phi\\
\phi:\Phi,~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x, ~ \b :\B~\phi~(\h_\n~\phi~\cblu{\partial}\x~\x)
\begin{multlined}[t]
\t_\n~\phi~\cblu{\partial}\x~\x~\b : (\X^{\cred{\partial}\n})\d~\pair{\phi}{\sigma~(\h_\n~\phi~\cblu{\partial}\x~\x)~\b}~\cblu{\partial}\x.
\end{multlined}
\end{align*}
The equation $\F\g_{\n+\cred{1}} \circ \x_{\n+\cred{2}} = \x_{\n+\cred{1}} \circ \g_{\n+\cred{2}}$ means that
\[\phi:\Phi,~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x,~\x\cblu{'} : \X^{\n+\cred{1}}~\phi~\sqbkt{\cblu{\partial}\x,\x}
\vdash
\h_{\n+\cred{1}}~\phi~\sqbkt{\cblu{\partial}\x, \x}~\x\cblu{'} \equiv \h_\n~\phi~\cblu{\partial}\x~\x\]
\begin{multline*}
\phi:\Phi,~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x,~\x\cblu{'} : \X^{\n+\cred{1}}~\phi~\sqbkt{\cblu{\partial}\x,\x},~\b :\B~\phi~(\h_\n~\phi~\cblu{\partial}\x~\x)\\
\vdash
\t_{\n+\cred{1}}~\phi~\sqbkt{\cblu{\partial}\x,\x}~\x\cblu{'}~\b
\equiv
\sqbkt{\t_\n~\phi~\cblu{\partial}\x~\x~\b,~ \s_\n~\phi~\cblu{\partial}\x~\x~\x\cblu{'}~\b }
\end{multline*}
for some term
\begin{multline*}
\phi:\Phi,~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~ \x : \X^\n~\phi~\cblu{\partial}\x,~\x\cblu{'} : \X^{\n+\cred{1}}~\phi~\sqbkt{\cblu{\partial}\x,\x},~\b :\B~\phi~(\h_\n~\phi~\cblu{\partial}\x~\x)\\
\vdash
\begin{multlined}[t]
\s_\n~\phi~\cblu{\partial}\x~\x~\x\cblu{'}~\b : (\X^\n)\d~\pair{\phi}{\sigma~(\h_\n~\phi~\cblu{\partial}\x~\x)~\b}~\pair{\cblu{\partial}\x}{\t_\n~\phi~\cblu{\partial}\x~\x~\b}~\x\\
\equiv(\X^\n)\d~\pair{\phi}{\sigma~(\h_{\n-\cred{1}}~\phi~\cblu{\partial}\x)~\b}~\pair{\cblu{\partial}\x}{\t_\n~\phi~\cblu{\partial}\x~\x~\b}~\x
\end{multlined}
\end{multline*}

Now inspecting the actual construction, we start with $\X_\cred{0} = \X^\cred{\partial 0} = \ec$, the empty telescope, and $\X^\cred{0} = \F(\X^\cred{\partial 0}) = \F\ec = \A$.
It is easy to see by induction that the functions $\h_\n$ then all just project to $\X^\cred{0}$.
For the rest, combining \cref{eq:xnplusone,eq:fgap}, we find that $\X^{\n+\cred{1}}$ is defined by
\begin{multline*}
\phi:\Phi , ~\cblu{\partial}\x : \X^{\cred{\partial}\n}~\phi,~\x:\X^\n~\phi~\cblu{\partial}\x \vdash\\
\begin{multlined}[t]
\X^{\n+\cred{1}}~\phi~\sqbkt{\cblu{\partial}\x,~\x} \equiv\\
(\b : \B~\phi~(\h_{\n-\cred{1}}~\phi~\cblu{\partial}\x)) \to  (\X^\n)\d~\pair{\phi}{\sigma~(\h_{\n-\cred{1}}~\phi~\cblu{\partial}\x)~\b}~\pair{\cblu{\partial}\x}{\t_\n~\phi~\cblu{\partial}\x~\x~\b}~\x
\end{multlined}
\end{multline*}
and we have tautologically
\[ \s_\n~\phi~\cblu{\partial}\x~\x~\x\cblu{'}~\b \equiv \x\cblu{'}~\b.\]
In particular, by induction we find that in fact each $\X^\n$, though by construction a telescope, is actually just a single type for all $\n\ge \cred{0}$.
Therefore, the tower $(\X^{\cred{\partial}\n},\X^\n)$ is precisely an infinite telescope as defined in \cref{sec:inftel}, which we denote
\[  \cblu{\Xtil} = (\X^{\cred{\partial}\n},\X^\n) .\]
Our display coinductive type is therefore precisely the limit of this infinite telescope as in \cref{sec:inflim}:
\[\dCoind(\Phi,\A,\B,\sigma)~\phi \equiv
\lim\bkt{ \cblu{\Xtil}~\phi}.  \]

\begin{example}
Recall that for semisimplicial types $\SST$, we have $\Phi\equiv\ec$, with $\A\equiv\Type$ and $\B~\a \equiv \El~\a$.
Therefore, in this case we have
\begin{align*}
\X^\cred{0} &\equiv \Type\\
\X^\cred{0}~\A_\cblu{0} &\equiv \El~\A_\cblu{0} \to \Type\d~\A_\cblu{0}\\
&\equiv \El~\A_\cblu{0} \to \El~\A_\cblu{0}\to \Type\\
\X^\cred{2}~\A_\cblu{0}~\A_\cblu{1} &\equiv
% (a_0:\El~\A_\cblu{0}) \to \dbkt{\El~A \to \El~A\to \Type}_{A:\Type}\d~A_0~(A_1~a_0)~A_1\\
(\a_\cblu{1}:\A_\cblu{0}) \to \dbkt{\A \to \A\to \Type}_{\A:\Type}\d~\A_\cblu{0}~(\A_\cblu{1}~\a_\cblu{1})~\A_\cblu{1}\\
\begin{multlined}[t]
(\a_\cblu{1}:\A_\cblu{0}) \to \dbkt{(\x:\A)(\x\cblu{'}:\A\cblu{'}~\x)(\y:\A)(\y\cblu{'}:\A\cblu{'}~\y) \to \Type\d~(\A\cblu{''}~\x~\y)}\\_{\A:\Type, \;\A\cblu{'}:\Type\d \A, \; \A\cblu{''} : \A\to \A \to \Type}~\A_\cblu{0}~(\A_\cblu{1}~\a_\cblu{1})~\A_\cblu{1}
\end{multlined}
\\
\begin{multlined}[t][0.8\linewidth]
(\a\sub{\cblu{001}}:\A_\cblu{0})(\a\sub{\cblu{010}}:\A_\cblu{0})(\a\sub{\cblu{011}}:\A_\cblu{1}~\a\sub{\cblu{001}}~\a\sub{\cblu{010}}) (\a\sub{\cblu{100}}:\A_\cblu{0}) (\a\sub{\cblu{101}}:\A_\cblu{1}~\a\sub{\cblu{001}}~\a\sub{\cblu{100}}) (\a\sub{\cblu{110}}:\A_\cblu{1}~\a\sub{\cblu{010}}~\a\sub{\cblu{100}}) \to \Type
\end{multlined}
\end{align*}
and so on: $\X^{\cred{\partial}\n}$ is the type of $(\n-\cred{1})$-truncated semisimplicial types, and $\X^\n~\A$ is the type of ways to extend such an $\A$ to an $\n$-truncated one, i.e.\ the types of indexed families of $\n$-simplices.
\end{example}

It remains to show that this construction of $\dCoind$ has the structure stipulated in \cref{sec:dcoind}.
To this end, we first unpack what it means for a type $\C\in \Ty(\Gamma\ce\lock_\trisq\ext\Phi)$ to be an $\Ftil$-coalgebra.
This means it is equipped with a section of the projection $\Ftil(\C) = (\C\ext \F(\C)) \to \C$, which syntactically is to say a partial substitution
\[ \Gamma,~\lock_\trisq\ext(\phi:\Phi), \x:\C \vdash \c : (\a:\A~\phi,~ \xp : (\b:\B~\phi~\a) \to \X\d~\pair{\phi}{\sigma~\a~\b}~\x).
\]
But this is equivalent to giving its components, which we abstract over $x$ to emphasise their dependence on it:
\begin{align*}
\Gamma,~\lock_\trisq\ext(\phi:\Phi) &\vdash \h : \C \to \A~\phi\\
\Gamma,~\lock_\trisq\ext(\phi:\Phi) &\vdash \t : (\x:\C) (\b:\B~\phi~(\h~\x)) \to \X\d~\pair{\phi}{\sigma~(\h~\x)~\b}~\x
\end{align*}
This is evidently precisely the structure of $\head$ and $\tail$ from \cref{sec:dcoind}.
Thus, our terminal $\Ftil$-coalgebra admits these destructors.

Furthermore, to give some other telescope $\Theta \in \Tel(\Gamma\ce\lock_\trisq\ext\Phi)$ an $\Ftil$-coalgebra structure is equivalent to equipping $\Upsilon \equiv (\Phi\ext\Theta)$ with the premises of the corecursor, where the indices-assigning map $\zeta : (\Phi\ext\Theta) \to \Phi$ is the dependent projection.
Thus, terminality of our terminal $\Ftil$-coalgebra implies that it admits the corecursor for telescopes $\Upsilon$ of this form.

In the models arising from type-theoretic model toposes, the underlying category is actually locally cartesian closed, and thus the functor $\Ftil$ can be extended from $\Telover(\Gamma\ce\lock_\trisq\Phi)$ to the larger slice category $(\Telover(\Gamma\ce\lock_\trisq))/\Phi$, with the same terminal coalgebra in this larger category.
This directly implies the full corecursion principle, since $\zeta$ in that rule equips $\Upsilon$ with the structure of an object of this slice.

In fact, the same is true for arbitrary models: the premises of the corecursor equip $\Upsilon$ with \emph{`enough of an $\Ftil$-coalgebra structure'} to deduce the existence of a unique compatible map to the terminal coalgebra.
In the next section we prove this in a more general abstract context.

\subsubsection{Terminal generalised coalgebras}
\label{sec:gener-term-coalg}

Let $\F$ be a copointed endofunctor of a category $\MC$ as in \cref{sec:term-coalg}, where $\MC$ is a full subcategory of some larger category $\E$.

\begin{definition}
An object $\Y\in \E$ is a \textbf{generalised $\F$-coalgebra} if it is equipped with:
\begin{itemize}
\item For any $\X\in \MC$ and morphism $\h:\Y\to \X$, a specified morphism $\overline{\h}: \Y \to \F\X$, such that
\item $\epsilon_\X \circ \overline{\h} = \h$.
\item For any $\g : \X \to \Z$ in $\MC$, we have $\F\g \circ \overline{\h} = \overline{\g\circ \h}$.
\end{itemize}
\end{definition}

In more abstract language, we can say that $F$ induces a copointed endofunctor $F^*$ of the functor category $\Set^\C$ by precomposition, and $Y$ is a generalised $F$-coalgebra if the functor $\E(Y,-) : \C \to \Set$ is an $F^*$-coalgebra.
The following observation is then a consequence of the Yoneda lemma, but we write it out explicitly.

\begin{lemma}
If $\Y\in\MC$, then generalised $\F$-coalgebra structures on $Y$ are bijective to ordinary $F$-coalgebra structures.
\end{lemma}
\begin{proof}
In one direction, if $\y:\Y\to \F\Y$ is an $\F$-coalgebra structure, then given $\h:\Y\to \X$ define $\overline{\h} = \F\h \circ \y$.
Then we have
\[\epsilon_\X \circ \overline{\h} = \epsilon_\X \circ \F\h \circ \y = \h\circ \epsilon_\Y \circ \y = \h \]
\[ \F\g \circ \overline{\h} = \F\g \circ \F\h \circ \y = \F(\g\circ \h) \circ \y = \overline{\g\circ \h}. \]

In the other direction, given a generalised $\F$-coalgebra structure, let $\y = \overline{\id_\Y}  : \Y \to \F\Y$.
Then $\epsilon_\Y \circ \y = \id_\Y$ by assumption, so $\y$ is an $\F$-coalgebra structure.
Moreover, the other axiom implies that for any $\g : \Y \to \Z$ we have $\overline{\g} = \overline{\g\circ \id_\Y} = \F\g \circ \overline{\id_\Y} = \F\g\circ \y$.
Thus one round-trip composite is the identity.
The other round-trip composite simply sends $\y :\Y \to \F\Y$ to $\overline{\id_\Y} = \F(\id_\Y) \circ \y = \id_{\F\Y}\circ \y = \y$.
\end{proof}

Of course, a \textbf{morphism of generalised $\F$-coalgebras} is a morphism $\f:\Y\to \Z$ such that for any $\h:\Z\to \X\in \MC$ we have $\overline{\h}\circ \f = \overline{\h\circ \f}$.

\begin{lemma}\label{thm:mor-gen-coalg}
If $\Y\in \E$ is a generalised $\F$-coalgebra and $\x:\X\to \F\X$ is an $\F$-coalgebra in $\MC$, then a morphism $\f:\Y\to \X$ is a generalised $\F$-coalgebra morphism if and only if $\overline{\f} = \x\circ \f$.
\end{lemma}
\begin{proof}
If it is a generalised $\F$-coalgebra map, then taking $\h = \id_\X$ in $\overline{\h}\circ \f = \overline{\h\circ \f}$ we get $\x\circ \f = \overline{\f}$.
On the other hand, if $\x\circ \f = \overline{\f}$ then for any $\h:\X\to \cblu{X'}$ in $\MC$ we have $\overline{\h} \circ \f = \cblu{x'} \circ \h \circ \f = \F\h \circ \x \circ \f = \F\h \circ \overline{\f} = \overline{\h\circ \f}$, as desired.
\end{proof}

\begin{theorem}\label{thm:termgencoalg}
Let $\MC$ and $\F$ be as in \cref{thm:termcoalg}, and let $\MC$ be a full subcategory of $\E$ such that the embedding preserves the terminal object and the inverse limits of $\omega$-sequences of fibrations.
Then the terminal $\F$-coalgebra constructed in \cref{thm:termcoalg} is also a terminal generalised $F$-coalgebra.
\end{theorem}
\begin{proof}
Indeed, the proof of terminality in \cref{thm:termcoalg} really only uses the generalised $\F$-coalgebra structure, which we can see clearly by repeating it in that language.
Let $\Y\in \E$ be a generalised $\F$-coalgebra.
We construct inductively maps $\h_\n : \Y \to \X_\n$ such that $\x_{\n+\cred{1}} \circ \h_{\n+\cred{1}} = \overline{\h_\cred{n}}$ and $\g_{\n+\cred{1}}\circ \h_{\n+\cred{1}} = \h_\n$.
We start with $\h_\cred{0} : \Y \to \X_\cred{0} = \One$ the unique morphism (since $1\in\MC$ is also terminal in $\E$), and $\h_\cred{1} = \overline{\h_\cred{0}} : \Y \to \X_\cred{1} = \F\X_\cred{0}$.
Then we induce $\h_{\n+\cred{1}}$ by the universal property of the pullback defining $\X_{\n+\cred{1}}$:
\[
\begin{tikzcd}
\Y \ar[ddr,bend right,"\h_\n"'] \ar[drr,bend left,"\overline{\h_\n}"] \ar[dr,dashed,"\h_{\n+\cred{1}}"] \\
&\X_{\n+\cred{1}} \ar[r,"\x_{\n+\cred{1}}"] \ar[d,"\g_{\n+\cred{1}}"] \drpullback & \F \X_\n \ar[d,"\leibhom{\epsilon}{\g_\n}"]\\
&\X_\n \ar[r,"{(\id,\;\x_\n)}"'] & \X_\n \times_{\X_{\n-\cred{1}}} \F \X_{\n-\cred{1}}.
\end{tikzcd}
\]
This is valid because using the inductive assumptions about $\h_\n$ and $\h_{\n-\cred{1}}$ and the properties of generalised coalgebras, we have
\begin{align*}
\epsilon_{\X_\n} \circ \overline{\h_\n} = \h_\n
\end{align*}
\begin{align*}
\F\g_{\n} \circ \overline{\h_\n}
&= \overline{\g_\n \circ \h_\n}\\
&= \overline{\h_{\n-\cred{1}}}\\
&= \x_\n \circ \h_\n,
\end{align*}
and the two triangles relating to $\h_{\n+\cred{1}}$ show that it has the necessary properties.

Now, the equations $\g_{\n+\cred{1}}\circ \h_{\n+\cred{1}} = \h_\n$ imply there is an induced map $\h_\cred{\infty} : \Y \to \X_\cred{\infty}$, such that $\x_\cred{\infty} \circ \h_\cred{\infty}$ is induced by the composites $\x_{\n+\cred{1}}\circ \h_{\n+\cred{1}}$.
But $\x_{\n+\cred{1}} \circ \h_{\n+\cred{1}} = \overline{\h_\n}$, and the morphisms $\F \h_\n$ induce the limit map $\F \h_\cred{\infty}$, so $\x_\cred{\infty} \circ \h_\cred{\infty} = \overline{\h_\cred{\infty}}$.
Thus, by \cref{thm:mor-gen-coalg}, $\h_\cred{\infty}$ is an $\F$-coalgebra morphism.

Finally, suppose $\k:\Y\to \X_\cred{\infty}$ is any $\F$-coalgebra morphism, so we have $\x_\cred{\infty} \circ \k = \overline{\k}$.
Then $\k$ is uniquely determined by the maps $\k_\n : \Y \to \X_\n$, and we have $\x_{\n+\cred{1}} \circ \k_{\n+\cred{1}} = \overline{\k_\n}$.
But this equation implies by induction that $\k_\n = \h_\n$ for all $\n$, hence $\k = \h_\cred{\infty}$.
\end{proof}

\subsubsection{The general corecursor}
\label{sec:general-corecursor}

Suppose $\Upsilon\in \Tel (\Gamma\ce\lock_\trisq)$ has the structure of the premises of the corecursor from \cref{sec:dcoind}:
\begin{align*}
\Gamma, \lock_\trisq\ext \upsilon:\Upsilon &\vdash \zeta~\upsilon : \Phi\\
\Gamma, \lock_\trisq\ext\upsilon:\Upsilon &\vdash \h~\upsilon : \A~{(\zeta~\upsilon)}\\
\Gamma, \lock_\trisq\ext \upsilon:\Upsilon\ext \y : \B{(\zeta\upsilon, \h)} &\vdash \tau~\upsilon~\y : {\Upsilon\d~\upsilon}\\
\Gamma, \lock_\trisq \ext \upsilon:\Upsilon \ext \y : \B{(\zeta\upsilon, \h)} &\vdash
\zeta\d~\pair{\upsilon}{\tau~\upsilon~\y} = \sigma~(\zeta~\upsilon)~(\h~\upsilon)~\y
\end{align*}
Then $\zeta$ makes it an object of the slice category $(\Telover(\Gamma\ce\lock_\trisq))/\Phi$.
We will apply \cref{thm:termgencoalg} to the full subcategory $\Telover (\Gamma\ce\lock_\trisq\ext\Phi) \subseteq (\Telover(\Gamma\ce\lock_\trisq))/\Phi$.
To that end, we give $\Upsilon$ the structure of a generalised $\Ftil$-coalgebra as follows.

Suppose $\X\in \Tel(\Gamma\ce\lock_\trisq\ext\Phi)$, and suppose we have a map $\g : \Upsilon \to \X$ in $(\Telover(\Gamma\ce\lock_\trisq))/\Phi$, which is to say
\[ \Gamma, \lock_\trisq\ext \upsilon:\Upsilon \vdash \g~\upsilon : \X~(\zeta~\upsilon). \]
We want to lift $\g$ to $\F \X$, which is to say we want to give
\begin{align*}
\Gamma, \lock_\trisq\ext(\upsilon:\Upsilon) &\vdash \h~\upsilon : \A~(\zeta~\upsilon)\\
\Gamma, \lock_\trisq\ext(\upsilon:\Upsilon),(\b:\B~\phi~(\h~\x)) &\vdash \t~\upsilon~\b : \X\d~\pair{\zeta~\upsilon}{\sigma~(\h~(\zeta~\upsilon)~(\g~\upsilon))~\b}~(\g~\upsilon)
\end{align*}
But such an $\h$ is exactly part of the structure of $\Upsilon$, while we can define
\[ \t~\upsilon~\b \equiv \g\d~\upsilon~(\tau~\upsilon~\b).
\]
The final equation in the structure of $\Upsilon$ is precisely what is necessary to make this well-typed.
The functoriality condition is immediate from the functoriality of $\d$.

Thus $\Upsilon$ is a generalised $\Ftil$-coalgebra, and hence it admits a unique generalised $\Ftil$-coalgebra morphism to the terminal $\Ftil$-coalgebra $\C$.
This is a map $\Upsilon \to (\Phi\ext \X)$ over $\zeta$, which is precisely the right type of $\corec$.
And by \cref{thm:mor-gen-coalg}, the fact that it is a generalised $\Ftil$-coalgebra map precisely gives it the correct computation rules. \bbox

\section{Conclusion and future work}
\label{sec:conclusion}

In this paper we have made two main contributions.
First, we have described \emph{Displayed Type Theory (dTT)}, a new kind of type theory that incorporates (unary) internal parametricity but guarded by a modality, and showed that any model of dependent type theory with countable Reedy limits can be lifted to a model of dTT using augmented semi-simplicial diagrams.
Because the latter are diagrams on an \emph{inverse} category, their type theory is more closely related to that of the original model, and indeed the original model sits inside our model of dTT at the discrete mode.
In particular, unlike other internally parametric type theories, dTT is compatible with classical axioms such as excluded middle and choice, as long as they are formulated at the discrete mode (or under the modality $\dia$), and can be used as an internal logic to reason about arbitrary $(\infty,1)$-toposes.

Secondly, inside dTT we have introduced a notion of \emph{display coinductive type}, where the output of a destructor can be a parametricity `computability witness' of the input, and showed that as a particular case of this notion we can define a type of \emph{semi-simplicial types}.
This yields a new approach to the long-standing open problem of representing infinitely coherent higher structures in type theory.
Relative to other approaches, ours has the advantage that semi-simplicial types are defined (not postulated) as a simple instance of a type-former with natural introduction and elimination rules, i.e.\ a categorical universal property.
While it remains to be seen how much can actually be done in practice with our definition, early indications of its utility are promising.

There are a number of directions for future work suggested by our results; here we survey a few of them briefly.

\paragraph{Modal internal parametricity.}

We expect that most applications of ordinary internal parametricity have modal versions that can be proven in dTT (or a higher-ary version of it, as discussed below).
In addition to the traditional `free theorems' such as those mentioned in the introduction, it would be especially interesting to investigate this for the proof of the pentagon identity for the smash product in~[10], since such a proof would then apply internally to any $(\infty,1)$-topos.

\paragraph{Higher category theory.}

We have \emph{defined} a type of semi-simplicial types in dTT, but such a definition is not an end in itself; it is intended as a tool for developing a theory of higher categories and other higher structures.
We hope that our corecursion principle of $\SST$, and the availability of other display coinductive types for predicates and structures on them, should make the development of such a theory feasible in dTT.
We sketched some initial ideas in \cref{sec:eg-sst,sec:exampl-displ-coind}, but much remains to be done.

\paragraph{Higher-ary dTT.}
\label{sec:higher-ary-dtt}

The parametricity of dTT is \emph{unary}, meaning that $\A\d$ depends on one copy of $\A$; but parametricity in general can be $\n$-ary for any natural number $\n$, and some applications require higher arities.
We expect that higher-ary versions of dTT can be defined and modeled by a straightforward modification of the constructions in this paper, using higher-ary semi-cubical types in place of augmented semi-simplicial types (recall that augmented semi-simplicial types are the same as unary semi-cubical types).
In this case the binary numbers described in \cref{sec:asscat} become base-$(\n+1)$ numbers.

\paragraph{Symmetries.}
\label{sec:symmetries}

In theories with non-modal internal parametricity, and also in Higher Observational Type Theory, it appears to be necessary to include a \emph{`symmetry'} operation on higher-dimensional types.
For instance, in our notation a symmetry operation would have the type $\A\d\d~\cblu{a\sub{00}}~\cblu{a\sub{01}}~\cblu{a\sub{10}}\to \A\d\d~\cblu{a\sub{00}}~\cblu{a\sub{10}}~\cblu{a\sub{01}}$.
The absence of symmetry in dTT is a significant simplification; for instance, it means that $\cred{\oldDelta^\cred{+}}\op$ is a strict inverse category, making possible the explicit syntactic model construction in \cref{sec:simplicial-model}.
However, we have also seen that it leads to certain limitations, e.g.\ without symmetry it is unclear how to give a corecursion principle for $\SST\d$.

It should be possible to formulate a version of dTT (unary or higher-ary) with symmetry, but in the presence of symmetry it is unclear whether it is possible for display to compute definitionally on type-formers.
However, it should work to use either the interval-based style of~[9, 8, 21] or the `observational' style of~[2].

\paragraph{Unimode dTT.}

We have formulated dTT with two modes, but intuitively the discrete mode is unnecessary, as the $\dm$-types are embedded in the $\sm$-types by the modality $\tri$.
Thus, it should be possible to formulate a version of dTT in which there is only one mode.
This is similar to other situations such as spatial/cohesive type theory~[25] and synthetic guarded domain theory~[15] that have both unimodal and bimodal versions.

\paragraph{Conjectural syntax.}
\label{subsec:conjectural-syntax}

In addition to display coinductive types, one may consider other kinds of generalized inductive and coinductive types.
These are especially useful when taking a more `synthetic' approach to higher structures in dTT, using the $\sm$-types as augmented semi-simplicial objects rather than working with the internally defined type $\SST$ of semi-simplicial types.

Firstly, regarding display as analogous to paths in homotopy type theory suggests \emph{displayed inductive types} as analogues of higher inductive types.
Here the constructors generate displayed elements rather than ordinary ones.
% \begin{lstlisting}
% (*\textbf{data}*) (*$\cred{\mathsf{Foo}}$*) : (*$\Type$*) (*\textbf{where}*)
%   (*$\cred{\oldalpha}$*) : (*$\cred{\mathsf{Foo}}$*)
%   (*$\cred{\beta}$*) : (*$\cred{\mathsf{Foo}}\d~\cred{\oldalpha}$*)
% (*$\f$*) : (*$\cred{\mathsf{Foo}}$*) (*$\to$*) (*$\A$*)
% (*$\f$*) (*$\cred{\oldalpha}$*) = (*?$_\oldalpha$*) : (*$\A$*)
% (*$\f\d$*) (*$\cred{\oldalpha}$*) (*$\cred{\beta}$*) = (*?$_\beta$*) : (*$\A\d$*) ((*$\f$*) (*$\cred{\oldalpha}$*))
% \end{lstlisting}
As an example, we can construct the simplicial cone of any type:\\
\begin{minipage}{\textwidth}
\begin{lstlisting}
(*\textbf{data}*) (*$\cred{\mathsf{C}}$*) ((*$\A$*) :(*$^\trisq$*) (*$\Type$*)) : (*$\Type$*) (*\textbf{where}*)
(*$\cred{\iota}$*) : (*$\A$*) (*$\to$*) (*$\cred{\mathsf{C}}$*) (*$\A$*)
(*$\cred{\oldsigma}$*) : ((*$\x$*) : (*$\A$*)) (*$\to$*) ((*$\cred{\mathsf{C}}$*) (*$\A$*))(*$\d$*) ((*$\cred{\iota}$*) (*$\x$*))

(*$\f$*) : (*$\cred{\mathsf{C}}$*) (*$\A$*) (*$\to$*) (*$\B$*)
(*$\f$*) ((*$\cred{\iota}$*) (*$\x$*)) = (*?$_\iota$*) : (*$\B$*)
(*$\f\d$*) ((*$\cred{\iota}$*) (*$\x$*)) ((*$\cred{\oldsigma}$*) (*$\x$*)) = (*?$_\oldsigma$*) : (*$\B\d$*) ((*$\f$*) ((*$\cred{\iota}$*) (*$\x$*)))
\end{lstlisting}
\end{minipage}

Secondly, regarding both display and paths as a kind of modality suggests considering more general \emph{modal inductive types}, whose constructors can land in modal versions of the type.
For instance, since $\dia\A$ is the $(\minusone)$-simplices of $\A$, a $\dia$-modal constructor adds a $(\minusone)$-simplex without any higher simplices above it.
In this way we can construct the free-living $(\minusone)$-simplex, and then all the higher simplices by coning:
\begin{lstlisting}
(*\textbf{data}*) (*$\cred{\Delta^{\minusone}}$*) : (*$\Type$*) (*\textbf{where}*)
(*$\cred{\star}$*) : (*$\dia$*) (*$\cred{\Delta^{\minusone}}$*)

(*$\f$*) : (*$\cred{\Delta^{\minusone}}$*) (*$\to$*) (*$\A$*)
(*$\dia$*) (*$\f$*) (*$\cred{\star}$*) = (*?$_\star$*) : (*$\dia$*) (*$\A$*)

(*$\cred{\Delta}$*) : (*$\cred{\mathbb{N}}$*) (*$\to$*) (*$\Type$*)
(*$\cred{\Delta}$*) (*$\cred{\mathsf{zero}}$*) = (*$\cred{\mathsf{C}}$*) (*$\cred{\Delta^{\minusone}}$*)
(*$\cred{\Delta}$*) ((*$\cred{\mathsf{suc}}$*) (*$\n$*)) = (*$\cred{\mathsf{C}}$*) ((*$\cred{\Delta}$*) (*$\n$*))
\end{lstlisting}

Note that in both cases, we rely on the computation behaviour of $\d$ and $\dia$ in order to directly give induction principles.\footnote{The case splits for defining a function $\f$ valued out of an inductive type in this hypothetical extension of \texttt{Agda}, as above, would result automatically by writing $\f~\x~=~?$ and pressing \texttt{C-c C-c} in the context of the hole.}
This is an improvement on the treatment of higher inductive types in~[28], since their natural elimination principle use $\mathsf{\cred{ap}}$, which is not there a primitive constant but a compound expression defined by path induction.
In particular, we conjecture that in dTT, these displayed and modal inductive types can be made fully computational.

\iffalse
\paragraph{An approach without GATs}
\label{subsec:gat-free}

In MLTT, contexts are telescopes of terms and substitutions may be defined as component term lists within a fixed context $\Gamma$, viz:
\begin{mathpar}
\infer{\ }{! : \Gamma \Rightarrow \ec}
\and
\infer{\sigma : \Gamma \Rightarrow \Theta \\ \Theta \vdash \A \type \\ \Gamma \vdash_\p \t : \A~\sqbkt{\sigma}}{\bkt{\sigma,~\t} : \Gamma \Rightarrow \bkt{\Theta,~\x:\A}}
\end{mathpar}
As with MTT, the approach that dTT takes above defines substitutions to be freely generated by constructions, such as formal composition, onto which we later impose relations. From this, it is not evident that a substitution is made up out of components. Indeed, in MTT, as presented in [15], no such decomposition of a substitution is known to be admitted by the theory. However, the particular mode theory $\cred{\M}$ of dTT is a special case of the arbitrary class of $\cred{2}$-categories considered by MTT, and this speciality allows us present an alternative theory in which substitutions are made out of components. We first set:
\begin{mathpar}
\infer{\Gamma \ctx_\p}{\u! : \Gamma \Rightarrow_\p \ec_\p}
\and
\infer{\mu\safe \\ \theta : \bkt{\Gamma,~\lock_{\mu^\dagger}} \Rightarrow_\q \Theta}{\widetilde{\theta} : \Gamma \Rightarrow_\p \bkt{\Theta,~\lock_\mu}}
\and
\infer{\theta : \Gamma \Rightarrow_\q \Theta \\ \Gamma,~\lock_\mu \vdash_\p \t : \A~\sqbkt{\theta,~\lock_\mu}}
{\bkt{\theta,~\t} : \Gamma \Rightarrow_\q \bkt{\Theta,~\x:^\mu \A}}
\end{mathpar}
If $\mu$ is hazardous, then a substitution $\Gamma \Rightarrow \bkt{\Theta,~\lock_{\mu}}$ may only be formed when $\Gamma$ is flat:
\begin{mathpar}
\infer{\mu\hazard \\ \Gamma\flat \\ \theta : \bkt{\Gamma,~\lock_{\mu^\dagger}} \Rightarrow_\q \Theta}{\widetilde{\theta} : \Gamma \Rightarrow_\p \bkt{\Theta,~\lock_\mu}}
\end{mathpar}
These rules uniquely define how to build $\Gamma \Rightarrow \Theta$, for a specific context presentation of $\Theta$.
This is sufficient if we specify a way of choosing canonical context presentations as discussed above.
Alternatively, if we decline to choose canonical presentations, then two different presentations of the same context can lead to two different presentations of what should be the same substitution, so the above rules for substitutions have to be quotiented by analogous equalities:
\begin{mathpar}
\widetilde{\theta} \equiv \theta
\and
\widetilde{\widetilde{\theta}} \equiv \widetilde{\theta}
\and
\widetilde{!}~\equiv~!
\end{mathpar}
in the cases of locking by $\id_\p$, locking by a composition $\mu \circ \nu$, and locking by $\sq$, respectively. Essentially, one may think of substitutions as consisting solely of components corresponding to the types in $\Theta$, with instances of adjointification notationally elided, although serving an important implicit role in updating the context $\Gamma$ with locks.

The appeal of such an approach is that it would most likely allow for an easier implementation of dTT in the guise of a computer proof assistant. The drawback, however, from a theoretical perspective, is that one would have to define how precisely every single algebraic substitution considered in our original presentation is made up out of components. What such a technical undertaking would essentially amount to is nothing short of a complete formalisation of the syntax of dTT within type theory, which would be a most laborious task. Moreover, a syntax first approach would also be further from semantics. Thus, it is clear that attempting such an exposition would negatively impact the clarity of this paper. However, if one accepted that certain syntactic coherences held on faith, this would be the optimal route to pursue in concrete computer implementations.
\fi

\bibliographystyle{alpha}
\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{AFM{\etalchar{+}}21}

[1]
Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler.
\newblock Two-level type theory and applications.
\newblock {\em Mathematical Structures in Computer Science}, page 1–56, 2023.
\newblock arXiv:1705.03307.

[2]
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman.
\newblock Internal parametricity, without an interval.
\newblock To appear in POPL'24. arXiv:2307.06448, 2024.

[3]
Peter Aczel.
\newblock The type theoretic interpretation of constructive set theory.
\newblock In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, {\em
Logic Colloquium '77}, volume~96 of {\em Studies in Logic and the Foundations
of Mathematics}, pages 55--66. Elsevier, 1978.

[4]
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccol\`o Veltri, and Niels van~der
\newblock Bicategories in univalent foundations.
\newblock {\em Mathematical Structures in Computer Science},
31(10):1232–1269, 2021.

[5]
Thorsten Altenkirch, Ambrus Kaposi, and Michael Shulman.
\newblock Towards a third-generation {HOTT}.
\newblock URL:
\url{https://ncatlab.org/nlab/show/higher+observational+type+theory}, 2022.

[6]
Benedikt Ahrens and Peter~LeFanu Lumsdaine.
\newblock Displayed categories.
\newblock {\em Logical Methods in Computer Science}, 15(1), March 2019.

[7]
Steve Awodey.
\newblock Natural models of homotopy type theory.
\newblock {\em Math. Structures Comput. Sci.}, 28(2):241--286, 2018.
\newblock arXiv:1406.3219.

[8]
Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin.
\newblock A presheaf model of parametric type theory.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 319:67 -- 82,
\newblock The 31st Conference on the Mathematical Foundations of Programming
Semantics (MFPS XXXI).

[9]
Jean-Philippe Bernardy and Guilhem Moulin.
\newblock A computational interpretation of parametricity.
\newblock In {\em Proceedings of the 2012 27th Annual IEEE/ACM Symposium on
Logic in Computer Science}, LICS '12, page 135–144, USA, 2012. IEEE
Computer Society.

[10]
Evan Cavallo.
\newblock {\em Higher Inductive Types and Internal Parametricity for Cubical
Type Theory}.
\newblock PhD thesis, Carnegie Mellon University, February 2021.

[11]
Simon Castellan, Pierre Clairambault, and Peter Dybjer.
\newblock Undecidability of equality in the free locally cartesian closed
category (extended version).
\newblock {\em Logical Methods in Computer Science}, 13(4), November 2017.

[12]
Simon Castellan, Pierre Clairambault, and Peter Dybjer.
\newblock Categories with families: Unityped, simply typed, and dependently
\newblock In Claudia Casadio and Philip~J. Scott, editors, {\em Joachim Lambek:
The Interplay of Mathematics, Logic, and Linguistics}, pages 135--180.
Springer Verlag, 2021.

[13]
Pierre Clairambault and Peter Dybjer.
\newblock The biequivalence of locally cartesian closed categories and
{Martin-L\"{o}f} type theories.
\newblock In {\em Proceedings of the 10th international conference on Typed
lambda calculi and applications}, TLCA'11, pages 91--106, Berlin, Heidelberg,
2011. Springer-Verlag.

[14]
Daniel Gratzer, Evan Cavallo, G.~A. Kavvos, Adrien Guatto, and Lars Birkedal.
\newblock Modalities and parametric adjoints.
\newblock {\em ACM Trans. Comput. Logic}, 23(3), apr 2022.

[15]
Daniel Gratzer, G.~A. Kavvos, Andreas Nuyts, and Lars Birkedal.
\newblock Multimodal dependent type theory.
\newblock {\em Logical Methods in Computer Science}, 17(3), July 2021.

[16]
G.~M. Kelly.
\newblock A unified treatment of transfinite constructions for free algebras,
free monoids, colimits, associated sheaves, and so on.
\newblock {\em Bull. Austral. Math. Soc.}, 22(1):1--83, 1980.

[17]
Krzysztof Kapulkin and Peter~LeFanu Lumsdaine.
\newblock Homotopical inverse diagrams in categories with attributes.
\newblock {\em Journal of Pure and Applied Algebra}, 225(4):106563, 2021.
\newblock arXiv:1808.01816.

[18]
Nicolai Kraus.
\newblock The general universal property of the propositional truncation.
\newblock In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, {\em
20th International Conference on Types for Proofs and Programs (TYPES 2014)},
volume~39 of {\em Leibniz International Proceedings in Informatics (LIPIcs)},
pages 111--145, Dagstuhl, Germany, 2015. Schloss Dagstuhl--Leibniz-Zentrum
fuer Informatik.
\newblock arXiv:1411.2682.

[19]
Ingrid {Lindstr\"om}.
\newblock A construction of non-well-founded sets within {Martin-L\"of's} type
\newblock {\em The Journal of Symbolic Logic}, 54(1):57–64, 1989.

[20]
Daniel~R. Licata, Ian Orton, Andrew~M. Pitts, and Bas Spitters.
\newblock Internal universes in models of homotopy type theory.
\newblock {\em Leibniz International Proceedings in Informatics (LIPIcs)},
108(22):1--17, 2018.
\newblock arXiv:1801.07664.

[21]
Guilhem Moulin.
\newblock {\em Internalizing parametricity}.
\newblock PhD thesis, Chalmers University, 2016.

[22]
Mitchell Riley, Eric Finster, and Daniel~R. Licata.
\newblock Synthetic spectra via a monadic and comonadic modality.
\newblock arXiv:2102.04099, 2021.

[23]
Emily Riehl and Michael Shulman.
\newblock A type theory for synthetic $\infty$-categories.
\newblock {\em Higher structures}, 1(1), 2017.
\newblock arXiv:1705.07442.

[24]
Michael Shulman.
\newblock Univalence for inverse diagrams and homotopy canonicity.
\newblock {\em Mathematical Structures in Computer Science}, 25(5):1203–1277,
June 2015.

[25]
Michael Shulman.
\newblock Brouwer's fixed-point theorem in real-cohesive homotopy type theory.
\newblock {\em Mathematical Structures in Computer Science}, 28(6):856--941,
\newblock arXiv:1509.07584.

[26]
Michael Shulman.
\newblock All $(\infty,1)$-toposes have strict univalent universes.
\newblock arXiv:1904.07004, 2019.

[27]
Michael Shulman.
\newblock Semantics of multimodal adjoint type theory.
\newblock {\em Electronic Notes in Theoretical Informatics and Computer
Science}, 3 (Proceedings of MFPS XXXIX), November 2023.
\newblock arXiv:2303.02572.

[28]
{Univalent Foundations Program}.
\newblock {\em Homotopy Type Theory: Univalent Foundations of Mathematics}.
\newblock \url{http://homotopytypetheory.org/book/}, first edition, 2013.

[29]
Elif Uskuplu.
\newblock {\em Formalizing two-level type theory with cofibrant exo-nat}.
\newblock PhD thesis, University of Southern California, 2023.

[30]
Philip Wadler.
\newblock Theorems for free!
\newblock In {\em Functional Programming Languages and Computer Architecture},
pages 347--359. ACM Press, 1989.

[31]
Jonathan Weinberger.
\newblock Strict stability of extension types.
\newblock arXiv:2203.07194, 2022.

\end{thebibliography}

\end{document}