\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{A'} \\
\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{B'} \\
\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}}
{\tcol{\GG} \vdash \tcol{t} \capre \tcol{\cast{A'}{B'}{t'}}}[Cast-R] \ilabel{infrule:capre-castr} \\
\inferrule{
\tcol{\sn{\GG}} \vdash \tcol{t'} \inferty \tcol{T'} \\
\tcol{\GG} \vdash \tcol{A} \cdpre \tcol{T'} \\
\tcol{\GG} \vdash \tcol{B} \cdpre \tcol{T'} \\
\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}}
{\tcol{\GG} \vdash \tcol{\cast{A}{B}{t}} \capre \tcol{t'}}[Cast-L] \ilabel{infrule:capre-castl} \\
\inferrule{\tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{T} \\ \tcol{\GG} \vdash \tcol{T} \cdpre \tcol{T'}}
{\tcol{\GG} \vdash \tcol{t} \capre \tcol{\?_{T'}}}[Unk] \ilabel{infrule:capre-unk} \and
\inferrule{\tcol{\fs{\GG}} \vdash \tcol{A} \pcheckty{[]} \tcol{[]_i} \\ i \leq j}
{\tcol{\GG} \vdash \tcol{A} \capre \tcol{\?_{[]_j}}}[Unk-Univ] \ilabel{infrule:capre-unk-univ} \and
\inferrule{\tcol{\sn{\GG}} \vdash \tcol{t'} \inferty \tcol{T'} \\ \tcol{\GG} \vdash \tcol{T} \cdpre \tcol{T'}}
{\tcol{\GG} \vdash \tcol{\err_{T}} \capre \tcol{t'}}[Err] \ilabel{infrule:capre-err} \and
\inferrule{\tcol{\fs{\GG}} \vdash \tcol{t'} \pcheckty{\Pi} \tcol{\P x : A' . B'} \\ \tcol{\GG} \vdash \tcol{\P x : A . B} \cdpre \tcol{\P x : A' . B'}}
{\tcol{\GG} \vdash \tcol{ \l x : A . \err_{B}} \capre \tcol{t'}}[Err-Lambda] \ilabel{infrule:capre-err-lambda}
\end{mathpar}
\boxedrule{$\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}$}
\begin{mathpar}
\hspace{6em}
\inferrule{\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}}{\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}} \and
\inferrule{\tcol{\GG} \vdash \tcol{s} \cdpre \tcol{t'} \\ \tcol{t} \redCCIC \tcol{s}}{\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}} \and
\inferrule{\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{s'} \\ \tcol{t'} \redCCIC \tcol{s'}}{\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}}
\end{mathpar}

\caption{Structural precision in \CCIC}
\label{fig:apre-ccic}
\end{figure}

Similarly to $$, precision can ignore some casts, in order to handle casts that might appear or disappear in one term but not the other
during reduction. But in order to control what
casts can be ignored, we impose some restriction on the types
involved. In particular, we want to ensure that ignored casts
would not have raised an error: \eg we want to prevent $0 0$.
Thus the definition of structural precision relies on typing, and to do this we need to record the contexts of the two compared terms. We do so by using double-struck letters to denote contexts where each variable is given two types, writing $, x : A |A'$ for context extensions. We use $_i$ for projections, \ie $(, x : A |A') := , x : A$, and write $Γ|Γ'$ for the converse pairing operation.

\begin{definition}[Structural and definitional precision in \CCIC]~

\emph{Structural precision}, denoted $\tcol{\GG} \vdash \tcol{t}
\capre \tcol{t'}$, is defined in \cref{fig:apre-ccic}, mutually with
\emph{definitional precision},
denoted $\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}$,
which is its closure by reduction.
We write $\tcol{\Gamma} \capre \tcol{\Gamma'}$ and $\tcol{\Gamma} \cdpre \tcol{\Gamma'}$ for the pointwise extensions of those to contexts.
\end{definition}
Although $ ⊢tt'$ is defined in a stepwise way, it is equivalent to the existence of $s$ and $s'$
such that $t s$, $t' s'$ and
$ ⊢s s'$.
The situation is the same as for consistency (\resp conversion), which
is the closure by reduction of $α$-consistency (\resp $α$-equality).
However, here definitional precision is also used in
the definition of structural precision, in order to permit
computation in types---recall that in a dependently-typed setting
the two types involved in a cast may need to reduce before the cast itself can
reduce---and thus the two notions are mutually defined.

Let us now explain the rules defining structural precision. Diagonal rules are completely structural, apart from the \nameref{infrule:capre-fix} rule, where typing assumptions provide us with the contexts needed to compare the predicates. More interesting are the non-diagonal rules.
First, $_T$ is greater than any term of the ''right type''. This incorporates loss of precision (rule \nameref{infrule:capre-unk}), and accommodates for a small bit of cumulativity (rule \nameref{infrule:capre-unk-univ}). This is needed because of technical reasons linked with possibility to form products between types at different levels.
On the contrary, the error is smaller than any term (rule \nameref{infrule:capre-err}), even in its extended form on $Π$-types (rule \nameref{infrule:capre-err-lambda}), with a typing premise similar to that of rule \nameref{infrule:capre-unk}.
Finally, casts on the right-hand side can be ignored as long as they
are performed on types that are \emph{less} precise than the type of the
term on the left (rule \nameref{infrule:capre-castr}). Dually, casts on the
left-hand side can be ignored as long as they are performed on types
that are \emph{more} precise than the type of the term on the right
(rule \nameref{infrule:capre-castl}).

\paragraph{Catch-up lemmas}
The fact that structural precision is a simulation relies on a series of lemmas that all have the same form: under the assumption that a term $t'$ is less precise than a term $t$ with a known head ($[]$, $$, $I$, $λ$ or $c$), the term $t'$ can be reduced to a term that either has the same head, or is some $$. We call these {\em catch-up} lemmas, as they enable the less precise term to catch up to the more precise one whose head is already known. Their aim is to ensure that casts appearing in a less precise term never block reduction, as they can always be reduced away.

The lemmas are established in a descending fashion: first, on the
universe in \cref{lem:catchup-univ}, then on other types in
\cref{lem:catchup-type}, and finally on terms, namely on $λ$-abstractions in \cref{lem:catchup-lambda} and inductive constructors in \cref{lem:catchup-cons}. Each time, the previously proven catch-up lemmas are used to reduce types in casts appearing in the less precise term, apart from \cref{lem:catchup-univ}, where the induction hypothesis of the lemma being proven is used instead.

\begin{lemma}[Universe catch-up]~\\
\label{lem:catchup-univ}
Under the hypothesis that $\tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$, if $\tcol{\GG} \vdash \tcol{[]_i} \cdpre \tcol{T'}$ and $\tcol{\sn{\GG}} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_{j}}$, either $\tcol{T'} \rtred \tcol{\?_{[]_{j}}}$ with $i < j$, or $\tcol{T'} \rtred \tcol{[]_i}$.
\end{lemma}

\begin{lemma}[Types catchup]
\label{lem:catchup-type}
Under the hypothesis that $\tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$, we have the following:
\begin{itemize}
\item if $\tcol{\GG} \vdash \tcol{\?_{[]_i}} \capre \tcol{T'}$ and $\tcol{\sn{\GG}} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_{j}}$, then $\tcol{T'} \rtred \tcol{\?_{[]_{j}}}$ and $i \leq j$;
\item if $\tcol{\GG} \vdash \tcol{\P x : A.B} \capre \tcol{T'}$, $\tcol{\fs{\GG}} \vdash \tcol{\P x : A. B} \inferty \tcol{[]_i}$ and $\tcol{\sn{\GG}} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_j}$ then either $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ and $i \leq j$, or $\tcol{T'} \rtred \tcol{\P x : A' . B'}$ for some $\tcol{A'}$ and $\tcol{B'}$ such that $\tcol{\GG} \vdash \tcol{\P x : A . B} \capre \tcol{\P x :A' . B'}$;
\item if $\tcol{\GG} \vdash \tcol{I(\orr{a})} \capre \tcol{T'}$, $\tcol{\fs{\GG}} \vdash \tcol{I(\orr{a})} \inferty \tcol{[]_i}$ and $\tcol{\sn{\GG}} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_j}$ then either $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ and $i \leq j$, or $\tcol{T'} \rtred \tcol{I(\orr{a'})}$ for some $\tcol{a'}$ such that $\tcol{\GG} \vdash \tcol{I(\orr{a})} \capre \tcol{I(\orr{a'})}$.
\end{itemize}
\end{lemma}

\begin{lemma}[$\lambda$-abstraction catch-up]~\\
\label{lem:catchup-lambda}
If $\tcol{\GG} \vdash \tcol{\l x : A . t} \capre \tcol{s'}$, where $\tcol{t}$ is not an error, $\tcol{\fs{\GG}} \vdash \tcol{\l x : A. t} \inferty \tcol{\P x : A.B}$ and $\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{\Pi} \tcol{\P x : A'. B'}$, then $\tcol{s'} \rtred \tcol{\l x : A'.t'}$ with $\tcol{\GG} \vdash \tcol{\l x : A . t} \capre \tcol{\l x : A'. t'}$.

This holds in \CCICP, \CCICs, and for terms without $\tcol{\?}$ in \CCICT.
\end{lemma}

\begin{lemma}[Constructors and inductive error catch-up]~\\
\label{lem:catchup-cons}
If $\tcol{\GG} \vdash \tcol{c(\orr{a},\orr{b})} \capre \tcol{s'}$, $\tcol{\fs{\GG}} \vdash \tcol{c(\orr{a},\orr{b})} \inferty \tcol{I(\orr{a})}$ and $\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{I} \tcol{I(\orr{a'})}$, then either $\tcol{s'} \rtred \tcol{\?_{I(\orr{a'})}}$ or $\tcol{s'} \rtred \tcol{c(\orr{a'},\orr{b'})}$ with $\tcol{\GG} \vdash \tcol{c(\orr{a},\orr{b})} \capre \tcol{c(\orr{a'},\orr{b'})}$.

\noindent Similarly, if $\tcol{\GG} \vdash \tcol{\?_{I(\orr{a})}} \capre \tcol{s'}$, $\tcol{\fs{\GG}} \vdash \tcol{\?_{I(\orr{a})}} \inferty \tcol{I(\orr{a})}$ and $\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{I} \tcol{I(\orr{a'})}$, then $\tcol{s'} \rtred \tcol{\?_{I(\orr{a'})}}$ with
\mbox{$\tcol{\GG} \vdash \tcol{I(\orr{a})} \cdpre \tcol{I(\orr{a'})}$}.
\end{lemma}

Note that for \cref{lem:catchup-cons}, we need to deal with unknown terms
specifically, which is not necessary for \cref{lem:catchup-lambda}
because the unknown term in a $Π$-type reduces to a $λ$-abstraction.

\cref{lem:catchup-lambda} deserves a more extensive discussion, because it is the critical point where the difference between the three variants of \CCIC manifests. In fact, it does not hold in full generality for \CCICT. Indeed, the fact that $i ≤ij$ and $j ≤ij$ is used crucially to ensure that casting from a $Π$-type into $$ and back does not reduce to an error, given the restrictions on types in \nameref{infrule:capre-castr}. This is the manifestation in the reduction of the embedding-projection property~\cite{newAhmed:icfp2018}. In \CCICT it holds only if one restricts to terms without $$, where such casts never happen. This is important with regard to conservativity, as elaboration produces terms with casts but without $$, and \cref{lem:catchup-lambda} ensures that for those precision is still a simulation, even in \CCICT.

\begin{example}[Catch-up of $\lambda$-abstraction]
\ilabel{ex:lambda-abstr-catch-up}
The following term $\tcol{t_i}$ illustrates these differences
\[\tcol{t_i} := \tcol{\cast{\nat \to \nat}{\nat \to \nat \Leftarrow \?_{[]_i}}{\l x : \nat . \natsuc(x)}}\]
where $\tcol{\nat}$ is taken at the lowest level, \ie to mean $\tcol{\nat\ulev{0}}$. Such terms appear naturally whenever a loss of precision happens on a function, for instance when elaborating a term like $\scol{\left(\asc{(\l x : \nat . \natsuc(x))}{\?}\right)~0}$. Now this term $\tcol{t_i}$ always reduces to
\[\tcol{\cast{\stalkCIC{i}{\Pi} \Leftarrow \?_{[]_i} \Leftarrow \stalkCIC{i}{\Pi} \Leftarrow \nat \to \nat}{\nat \to \nat}{\l x : \nat . \natsuc(x)}}\]
and at this point the difference kicks in: if $\tcol{\stalkCIC{i}{\Pi}}$ is $\tcol{\err_{\?_{[]_i}}}$ (\ie if $\castOfPi{i} < 0$) then the whole term reduces to $\tcol{\err_{\nat \to \nat}}$. Otherwise, further reductions finally give
\[\tcol{\l x : \nat . \natsuc\left(\cast{\nat \Leftarrow \nat}{\nat}{x}\right) }\]
Although the body is blocked by the variable $\tcol{x}$, applying the function to $\tcol{0}$ would reduce to $\tcol{1}$ as expected. Let us compare what happens in the three systems.

In all of them, if $i \geq 1$, we have $\vdash \tcol{\l x : \nat . \natsuc(x)} \capre \tcol{t_i}$ via repeated uses of \nameref{infrule:capre-castr} since $\inferelab{}{\nat}{}{}{\nat}{[]_{\sortOfPi{0}{0}}}$ and $\sortOfPi{0}{0} \leq 1 \leq i$.
Moreover, also $0 \leq i - 1 \leq \castOfPi{i}$ and so the reduction is errorless.
Thus \cref{lem:catchup-lambda} holds in all three systems when $i \geq 1$.

The difference appears in the specific case where $i = 0$.
In \CCICP and \CCICT, we still have $\vdash \tcol{\l x : \nat . \natsuc(x)} \capre \tcol{t_0}$, since $\sortOfPi{0}{0} = 0 \leq i$. In the former, $\castOfPi{0} = 0$ so $\tcol{t_0}$ reduces safely and \cref{lem:catchup-lambda} holds. In the latter, however, $\castOfPi{0} = -1$,
and so $\tcol{t_0}$ errors even if it is less precise than an errorless term---\cref{lem:catchup-lambda} does not hold in that case.
Finally, in \CCICs, $\tcol{t_0}$ errors since again $\castOfPi{0} = -1$.
However, because $s_{\Pi}(0,0) = 1$, $\tcol{t_0}$ is not less precise than $\tcol{\l x : \nat. \natsuc(x)}$ thanks to the typing restriction in \nameref{infrule:capre-castr}, so this error does not contradict \cref{lem:catchup-lambda}.

\end{example}

Note that in an actual implementation with typical ambiguity (\cref{note:typ-amb}),
the case where $i = 0$ would most likely not manifest: elaborating
$((łx : . (x))) 0$ would produce a fresh
level that could be chosen high enough so as to prevent the error we just described.
Only more involved situations like that of $Ω$ (\cref{sec:back-to-omega}) would actually exhibit
failures due to universe levels, which are precisely those unavoidable to ensure normalization.

\paragraph{Simulation}
We finally come to the main property of this section, the advertised
Remark that the simulation property needs to be stated (and proven) mutually for structural and definitional precision, but it is really informative only for
structural precision (definitional precision is somehow a
simulation by construction).

\begin{theorem}[Precision is a simulation for reduction]~\\
\label{thm:simulation}
Let $\tcol{\fs{\GG}} \cdpre \tcol{\sn{\GG}}$, $\tcol{\fs{\GG}} \vdash \tcol{t}
\inferty \tcol{T}$, $\tcol{\sn{\GG}} \vdash \tcol{u} \inferty
\tcol{U}$ and $\tcol{t} \rtred \tcol{t'}$. Then
\begin{itemize}
\item
if $\tcol{\GG} \vdash \tcol{t} \capre \tcol{u}$ then there exists $\tcol{u'}$ such that $\tcol{u} \rtred \tcol{u'}$ and $\tcol{\GG} \vdash \tcol{t'} \capre \tcol{u'}$;
\item
if $\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{u}$ then
$\tcol{\GG} \vdash \tcol{t'} \cdpre \tcol{u}$.
\end{itemize}
This holds in \CCICP,
\CCICs and for terms without $\tcol{\?}$ in \CCICT.
\end{theorem}

\begin{proof}[Proof sketch]
The case of definitional precision follows by confluence of
For the case of structural precision, the hardest point is to simulate $\beta$ and $\iota$ redexes---terms of the shape $\match{I}{c(\orr{a})}{z.P}{f.\orr{y}.\orr{t}}$. This is where we use \cref{lem:catchup-lambda,lem:catchup-cons}, to show that similar reductions can also happen in $\tcol{t'}$.
We must also put some care into handling the premises of precision where typing is involved. In particular, subject reduction is needed to relate the types inferred after reduction to the type inferred before, and the mutual induction hypothesis on $\cdpre$ is used to conclude that the premises holding on $\tcol{t}$ still hold on $\tcol{t'}$.
Finally, the restriction to terms without $\tcol{\?}$ in \CCICT similar to \cref{lem:catchup-lambda} appears again when treating \nameref{redrule:up-down}, where having $\castOfPi{\sortOfPi{i}{i}} = i$ is required.
\end{proof}

From this theorem, we get as direct corollaries the following properties, that are required to handle reduction (\cref{cor:red-types}) and consistency (\cref{cor:mon-cons}) in elaboration. Again those corollaries hold in \GCICP, \GCICs and for terms in \GCICT containing no $$.

\begin{corollary}[Monotonicity of reduction to type constructor]~\\
\label{cor:red-types}
Let $\tcol{\GG}$, $\tcol{T}$ and $\tcol{T'}$ be such that $\tcol{\fs{\GG}} \vdash \tcol{T}  \pcheckty{[]} \tcol{\square{}_i}$, $\tcol{\sn{\GG}} \vdash \tcol{T'} \pcheckty{[]} \tcol{\square{}_j}$, $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$. Then
\begin{itemize}
\item if $\tcol{T} \rtred \tcol{\?_{[]_i}}$ then $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ with $i \leq j$;
\item if $\tcol{T} \rtred \tcol{\square{}_{i-1}}$ then either $\tcol{T'} \rtred \tcol{\?_{\square{}_j}}$ with $i \leq j$, or $\tcol{T'} \rtred \tcol{\square{}_{i-1}}$;
\item if $\tcol{T} \rtred \tcol{\P x : A. B}$ then either $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ with $i \leq j$, or $\tcol{T'} \rtred \tcol{\P x : A'. B'}$ and\\
\mbox{$\GG \vdash \tcol{\P x : A.B} \capre \tcol{\P x : A'.B'}$};
\item if $\tcol{T} \rtred \tcol{I(\orr{a})}$ then either $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ with $i \leq j$, or $\tcol{T'} \rtred \tcol{I(\orr{a'})}$ and $\GG \vdash \tcol{I(\orr{a})} \capre \tcol{I(\orr{a'})}$.
\end{itemize}
\end{corollary}

\begin{proof}
It suffices to simulate the reductions of $\tcol{T}$ by using \cref{thm:simulation}, and then use \cref{lem:catchup-type,lem:catchup-univ} to conclude. Note that head reductions are simulated using head reductions in \cref{thm:simulation}, and the reductions of \cref{lem:catchup-type,lem:catchup-univ} are also head reductions. Thus the corollary still holds when fixing weak-head reduction as a reduction strategy.
\end{proof}

\begin{corollary}[Monotonicity of consistency]
\label{cor:mon-cons}
If $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$, $\tcol{\GG} \vdash \tcol{S} \capre \tcol{S'}$ and $\tcol{T} \cons \tcol{S}$ then $\tcol{T'} \cons \tcol{S'}$.
\end{corollary}

\begin{proof}
By definition of $\cons$, we get some $\tcol{U}$ and $\tcol{V}$ such that $\tcol{T} \rtred \tcol{U}$ and $\tcol{S} \rtred
\tcol{V}$, and $\tcol{U} \acons \tcol{V}$. By \cref{thm:simulation},
we can simulate these reductions to get some $\tcol{U'}$ and $\tcol{V'}$ such that $\tcol{T'} \rtred \tcol{U'}$ and $\tcol{S'} \rtred \tcol{V'}$, and also $\tcol{\fs{\GG}} \vdash \tcol{U} \capre \tcol{U'}$ and $\tcol{\fs{\GG}} \vdash \tcol{V} \capre \tcol{V'}$. Thus we only need to show that $\alpha$-consistency is monotone with respect to structural precision, which is direct by induction on structural precision.
\end{proof}

\subsection{Properties of \GCIC}
\label{sec:gcic-theorems2}

We now have enough technical tools to prove most of the properties of \GCIC.
We state those theorems in an empty context in this section to make
them more readable, but they are of course corollaries of similar
statements including contexts, proven by mutual induction. The complete
statements and proofs can be found in \cref{sec:properties-gcic}.

\paragraph{Conservativity with respect to \CIC}
Elaboration systematically inserts casts during checking, thus even
static terms are not elaborated to themselves. Therefore we use a
(partial) erasure function $$ that translates terms of \CCIC to terms of \CIC by erasing all casts. We also introduce the notion of erasability, characterizing terms that contain ``harmless'' casts, such that in particular the elaboration of a static term is always erasable.

\begin{definition}[Equiprecision]
\label{def:equipre}
Two terms $\tcol{s}$ and $\tcol{t}$ are equiprecise in a context $\tcol{\GG}$, denoted $\tcol{\GG} \vdash \tcol{s} \caequipre \tcol{t}$ if both $\tcol{\GG} \vdash \tcol{s} \capre \tcol{t}$ and $\tcol{\GG} \vdash \tcol{t} \capre \tcol{s}$.
\end{definition}

\begin{definition}[Erasure, erasability]
\label{def:erasure}
Erasure $\eras$ is a partial function from the syntax of \CCIC to the syntax of \CIC, which is undefined on $\tcol{\?}$ and $\tcol{\err}$, is such that $\eras(\tcol{\cast{A}{B}{t}}) = \eras(\tcol{t})$, and is a congruence for all other term constructors.

Given a context $\tcol{\GG}$ we say that a term well-typed in $\tcol{\GG_1}$ $\tcol{t}$ is erasable if $\eras(\tcol{t})$ is defined, well-typed in $\tcol{\GG_2}$, and equiprecise to $\tcol{t}$ in $\tcol{\GG}$. Similarly a context $\tcol{\Gamma}$ is called erasable if it is pointwise erasable. When $\tcol{\Gamma}$ is erasable, we say that a term $\tcol{t}$ is erasable in $\tcol{\Gamma}$ to mean that it is erasable in $\tcol{\Gamma} \mid \eras(\tcol{\Gamma})$.
\end{definition}

Conservativity holds in all three systems, typeability being of course taken into the corresponding variant of \CIC: full \CIC for \GCICP and \GCICT, and \CICs for \GCICs.

\begin{theorem}[Conservativity]
\label{thm:conservativity}
Let $\scol{\tilde{t}}$ be a static term (\ie is a term of \GCIC that is also a term of \CIC).
If $\cicty \scol{\tilde{t}} \inferty T$ for some type $T$,
then there exists $\tcol{t}$ and $\tcol{T'}$ such that
$\inferelab{}{\tilde{t}}{}{}{t}{T'}$, and
moreover $\eras(\tcol{t}) = \scol{\tilde{t}}$ and $\eras(\tcol{T'}) = T$. Conversely if $\inferelab{}{\tilde{t}}{}{}{t}{T}$ for some $\tcol{t}$ and $\tcol{T}$, then $\cicty \scol{\tilde{t}} \inferty \eras(\tcol{T})$.
\end{theorem}

\begin{proof}[Proof sketch]

Because $\scol{t}$ is static, its typing derivation in \GCIC can only use rules that have a counterpart in \CIC, and conversely all rules of \CIC have a counterpart in \GCIC. The only difference is about the reduction/conversion side conditions, which are used on elaborated types in \GCIC, rather than their non-elaborated counterparts in \CIC.

Thus, the main difficulty is to ensure that the extra casts
inserted by elaboration do not alter reduction. For this we
maintain the property that all terms $\tcol{t}$ considered in
\CCIC are erasable, and in particular that any static term $\scol{{t}}$
that elaborates to some $\tcol{t}$ is such that
$\eras(\tcol{t}) = \scol{{t}}$. From the simulation property of
structural precision (\cref{thm:simulation}), we get that an
erasable term $\tcol{t}$ has the same reduction behavior as
its erasure, \ie if $\tcol{t} \rtred \tcol{s}$ then
$\eras(\tcol{t}) \rtred s'$ with $s'$ and $\tcol{s}$
equiprecise, and conversely if $\eras(\tcol{t}) \rtred s'$
then $\tcol{t} \rtred \tcol{s}$ with $s'$ and $\tcol{s}$
equiprecise. Using that property, we  prove that
constraint reductions ($\pcheckty{\Pi}$, $\pcheckty{[]}$ and
$\pcheckty{I}$) in \CCIC and \CIC behave the same on static terms.
\end{proof}

\paragraph{Elaboration Graduality}

\begin{figure}
\begin{mathpar}
\inferrule{ }{\scol{x} \apre \scol{x}} \and
\inferrule{ }{\scol{[]_i} \apre \scol{[]_i}} \and
\inferrule{\scol{A} \apre \scol{A'} \\ \scol{B} \apre \scol{B'}}
{\scol{\P x : A . B} \apre \scol{\P x : A'.B'}} \and
\inferrule{\scol{A} \apre \scol{A'} \\ \scol{t} \apre \scol{t'}}
{\scol{\l x : A . t} \apre \scol{\l x : A . t}} \and
\inferrule{\scol{t} \apre \scol{t'} \\ \scol{u} \apre \scol{u'}}{\scol{t~u} \apre \scol{t'~u'}} \and
\inferrule{\scol{\orr{a}} \apre \scol{\orr{a'}}}{\scol{I(\orr{a})} \apre \scol{I(\orr{a'})}} \and
\inferrule{\scol{\orr{a}} \apre \scol{\orr{a'}} \\ \scol{\orr{\scol{b}}} \apre \scol{\scol{\orr{b'}}}}{\scol{c(\orr{a},\orr{b})} \apre \scol{c(\orr{a'},\orr{b'})}} \and
\inferrule{\scol{a} \apre \scol{a'} \\ \scol{P} \apre \scol{P'} \\ \scol{\orr{t}} \apre \scol{\orr{t'}}}
{\scol{\match{I}{a}{z.P}{\orr{f.y.t}}} \apre \scol{\match{I}{a'}{z.P'}{\orr{f.y.t'}}}} \and
\inferrule{ }
{\scol{t} \apre \scol{\?}}
\end{mathpar}
\caption{Syntactic precision for \GCIC}
\label{fig:apre-gcic}
\end{figure}

Next, we turn to elaboration graduality, the equivalent of the static gradual
guarantee (SGG) of \citet{siekAl:snapl2015} in our setting.
We state it with respect to a notion of precision for terms in \GCIC,
\emph{syntactic precision} $$, defined in \cref{fig:apre-gcic}.
Syntactic precision is the usual and expected source-level notion of precision in gradual languages: it is generated by a single non-trivial rule $t i$, and congruence rules for all term formers.

In contrast with the simply-typed setting, the presence of multiple unknown types $$,
one for each universe level $i$, requires an additional hypothesis relating elaboration
and precision.
We say that two judgments $t̃ i$ and
$t̃ΓtT$ are \emph{universe adequate} if the
universe level $j$ given by the well-formedness judgment $Γ ⊢T
□ □_j$ induced by correction of the elaboration satisfies $i = j$.
More generally, $t̃ s̃$ and
$t̃tT$ are \emph{universe adequate} if for any
subterm $t̃_0$ of $t̃$ inducing judgments $t̃_0
i$ and $t̃_0Γ_0tT$, those are
universe adequate.
Note that this extraneous technical assumption on universe levels is not needed if we use typical ambiguity (\cref{note:typ-amb}),
since universe levels are not given explicitly.

\begin{theorem}[Elaboration Graduality / Static Gradual Guarantee]
\label{thm:static-graduality}
In \GCICP and \GCICs, if $\scol{\tilde{t}} \apre \scol{\tilde{s}}$ and
$\sinferelab{}{\tilde{t}}{}{}{t}{T}$ are universe adequate, then $\sinferelab{}{\tilde{s}}{}{}{s}{S}$ for some $\tcol{s}$ and $\tcol{S}$ such that $\vdash \tcol{t} \capre \tcol{s}$ and $\vdash \tcol{T} \capre \tcol{S}$.
\end{theorem}

\begin{proof}[Proof sketch]
The proof is by induction on the elaboration derivation for $\scol{\tilde{t}}$. All cases for inference consist in a straightforward combination of the hypotheses, with the universe adequacy hypothesis used in the case where $\scol{\tilde{s}}$ is $\scol{\?\ulev{i}}$.
Here again the technical difficulties arise in the rules involving reduction. This is where \cref{cor:red-types} is useful, proving that the less structurally precise term obtained by induction in a constrained inference reduces to a less precise type. Thus either the same rule can still be used, or one has to trade a \nameref{infrule:gcic-inf-univ}, \nameref{infrule:gcic-inf-prod} or \nameref{infrule:gcic-inf-ind} rule respectively for a \nameref{infrule:gcic-univ-unk}, \nameref{infrule:gcic-prod-unk} or \nameref{infrule:gcic-ind-unk} rule in case the less precise type is some $\tcol{\?_{[]_i}}$ and the more precise type is not. Similarly, \cref{cor:mon-cons} proves that in the checking rule the less precise types are still consistent.
Note that again, because \cref{cor:red-types} holds when restricted to weak-head reduction, elaboration graduality also holds when fixing a weak-head strategy in \cref{fig:elaboration}.
\end{proof}

\paragraph{Dynamic Gradual Guarantee}

Following \citet{siekAl:snapl2015}, using the fact that structural precision is
a simulation (\cref{thm:simulation}), we can prove the DGG for \CCICP
and \CCICs (stated using the notion of observational refinement
$$ from \cref{def:obsref}).

\begin{theorem}[Dynamic Gradual Guarantee for \CCICP and \CCICs]
\label{thm:dgg}
Suppose that $\tcol{\Gamma} \vdash \tcol{t}
\inferty \tcol{A}$ and $\tcol{\Gamma} \vdash \tcol{u} \inferty
\tcol{A}$.
If moreover $\tcol{\Gamma \mid \Gamma} \vdash \tcol{t} \capre \tcol{u}$ then $\tcol{t} \obsRef \tcol{u}$.
\end{theorem}
\begin{proof}
Let $\tcol{\mathcal{C}} : (\tcol{\Gamma} \vdash \tcol{A}) \Rightarrow (\vdash \tcol{\bool})$
closing over all free variables.
By the diagonal rules of structural precision, we have
$\tcol{\Gamma \mid \Gamma} \vdash \tcol{\mathcal{C}[t]} \capre \tcol{\mathcal{C}[u]}$.
By progress (\cref{thm:ccic-psafe}), $\tcol{\mathcal{C}[t]}$ either reduces
to $\tcol{\btrue}$, $\tcol{\bfalse}$, $\tcol{\?_{\bool}}$, $\tcol{\err_{\bool}}$ or diverges, and similarly for $\tcol{\mathcal{C}[u]}$.
If $\tcol{\mathcal{C}[t]}$ diverges or reduces to $\tcol{\err_\bool}$, we are done.
If it reduces to either $\tcol{\btrue}$, $\tcol{\bfalse}$ or $\tcol{\?_\bool}$, then by the catch-up \cref{lem:catchup-cons},
$\tcol{\mathcal{C}[u]}$ either reduces to the same value, or
to $\tcol{\?_\bool}$. In particular, it cannot diverge or reduce to
an error.
\end{proof}

Note that \cref{ex:lambda-abstr-catch-up} provides a counter-example to this theorem for \CCICT, by choosing the context $∙ 0z.f.,f.n.$, because in that context the function $łx : . (x)$ reduces to $$ while the less precise casted function reduces to $_$.

As observed in \cref{sec:grad-simple},
graduality---and in particular the fact that precision induces \eppairs{}---is inherently semantic, and thus cannot rely on the syntactic precision $$ introduced in this section.
Therefore, we defer the proof of \pgrad for \CCICs and \CCICP to the next
section, where the semantic notion of {\em propositional precision} is introduced.

\section{Realizing \CCIC and Graduality}
\label{sec:realizing-cast-calculus}
\label{sec:realizing-ccic}
To prove normalization of \CCICT and \CCICs, we now build a model of both
theories with a simple implementation of casts using case-analysis on types as well
as exceptions, yielding the \emph{\bareModel}, allowing us to reduce the
normalization of both theories to the normalization of the target theory

Then, to prove graduality of \CCICs,
we build a more elaborate \emph{monotone model} inducing a
precision relation well-behaved with respect to conversion.
Following generalities about the interpretation of \CIC's types as posets
in~\cref{sec:poset-model-dtt}, we describe the construction of a monotone
unknown type $$ in~\cref{sec:realizing-unknown-type} and a hierarchy of
universes in~\cref{sec:monotone-universe} and put these pieces together
in~\cref{sec:monotone-model}, culminating in a proof of graduality
for \CCICs (\cref{sec:grad-term}).
In both the discrete and monotone case, the parameters $-$ and
appear when building the hierarchy of universes and tying the knot with the
unknown type.

Finally, to deduce graduality for the non-terminating variant, \CCICP,
we describe at the end of this section a model based on
$ω$-complete partial orders, extending the seminal
model of \citet{scott76} for $λ$-calulus to \CCICP (\cref{sec:grad-non-term}).

The discrete model embeds into a variant of \CIC extended with
induction-recursion~\cite{DybjerS03}, noted \CICIR, and the monotone model into a variant that additionally features quotients (and hence also function extensionality~\cite{ShulmanIntervalFunext}), noted \CICIRQ.

\paragraph{Formalization in \Agda}
We use \Agda{}~\cite{norell:afp2008} as a practical tool to typecheck
the components of the models and assume that \Agda{} satisfies
standard metatheoretical properties, namely subject reduction and
strong normalization.

The correspondence between the notions developed in the following
sections and the formal development in \Agda{}~\cite{GCICAgdaCode} is as follows.
The formalization covers most component of the discrete
(\texttt{DiscreteModelPartial.agda}) and monotone model
(\texttt{UnivPartial.agda}) in a partial (non-normalizing) setting and only
the discrete model is proved to be normalizing assuming normalization of the
type theory implemented by Agda (no escape hatch to termination checking is
used in \texttt{DiscreteModelTotal}).
The main definitions surrounding posets can be found in \texttt{Poset.agda}:
top and bottom elements (called \texttt{Initial} and \texttt{Final} in the
formalization), embedding-projection pairs (called \texttt{Distr}) as well as
the notions corresponding to indexed families of posets
(\texttt{IndexedPoset}, together with \texttt{IndexedDistr}). It is then
proved that we endow can the translation of each type
formers from \CCIC{} with a poset structure: natural numbers in \texttt{nat.agda}, booleans in
\texttt{bool.agda}, dependent product in \texttt{pi.agda}. The definition of
the monotone unknown type \unkMon{} is defined in the subdirectory
\texttt{Unknown/}. It is more involved since we need to use a
quotient (that we axiomatize together with a rewriting rule in
\texttt{Unknown/Quotient.agda}).
Finally, all these building blocks are put together when assembling the
inductive-recursive hierarchies of universes (\texttt{UnivPartial.agda},
\texttt{DiscreteModelPartial.agda} and \texttt{DiscreteModelTotal.agda}).

\subsection{Discrete Model of \CCIC}
\label{sec:bare-model}

The discrete model explains away the new term formers of
\CCIC~(\ref{fig:syntax-castcic}) by a translation into \CIC{} using two important ingredients from the literature:
\begin{itemize}
\item Exceptions, following the approach of \ExTT~\cite{pedrotTabareau:esop2018}: each inductive type is extended with two new constructors, one for $\?$ and one for $\err$.
As alluded to early on (\cref{sec:graduality}), both $\?$ and $\err$ are exceptional terms in their propagation semantics, and only differ in their static interpretation: \coqe{?_A} is consistent with any other term of type \coqe{A}, while \coqe{err_A} is not consistent with any such term.

\item Case analysis on types~\cite{BoulierPT17} to define the cast operator. The
essence of the translation is to interpret types as {\em codes} when they are
seen as terms, and as {\em the semantics of those codes} when they are seen as
This allows us to get the standard interpretation for a term inhabiting
a type, but at the same time, it allows functions taking terms in the universe
$\U{}_i$ to perform a case analysis on the code of the type, because this
time, the type is seen as a term in $\U{}_i$.
\end{itemize}

The latter ingredient for intensional type
analysis requires the target theory of the translation to be an extension of
\CIC with induction-recursion~\cite{DybjerS03}, noted \CICIR. We write $$
and $$ to denote the reduction and typing judgments of \CICIR,

\paragraph{Inductive types}
Following the general pattern of \ExTT, we interpret each inductive type $I$ by
an inductive type $I$ featuring all constructors of $I$
and extended with two new constructors
$I$ and $I$, corresponding respectively to
$_I$ and $_I$ of \CCIC.
The constructors $I$ and $I$ of
$I$ are called \emph{exceptional} by opposition to the other
constructors that we call \emph{non-exceptional}.
For instance, the inductive type used to interpret natural numbers,
$$, thus has 4 constructors: the non-exceptional constructors $0$
and $$, and the exceptional
constructors $$, $$.
In the rest of this section, we only illustrate inductive types on natural numbers.

\paragraph{Universe and type-case}
Case analysis on types is obtained through an explicit inductive-recursive description of
the universes \cite{itt,McBride10} to build a type of codes $_i$
described in \cref{fig:discrete-univ}.
Codes are noted with $·$ and the universe type contains codes for
dependent product ($$), universes ($_j$), inductive types (\eg $$) as well as $$ for the unknown type and $$ for the error type. The main subtlety here is that the code $ A B$ is at level $ij$
when $A$ is at $i$ and $B$ is a family at $j$, emulating the rule of
\cref{fig:ccic-typing}.
Accompanying the inductive definition of $_i$, the recursively defined
decoding function $$ provides a semantics for these codes.
The semantics of $$ is given by the dependent product in the target theory,
applying $$ on the domain and the codomain of the code.
The semantics of $_j$ is precisely the type of codes $_j$.
The semantics of $$ is given by the extended natural numbers $$, explained above.

Intuitively, the semantics of $[i]$ is that an inhabitant of
the unknown type corresponds to a pair of a type and an inhabitant of
that type. More precisely, we first define a notion of germ for codes where we stratify the head constructors $$̋ (see <ref>) according to the
universe level $i$, e.g.
$\stalkCode{i}{\Pi} := \PiU\,\uU_{\castOfPi{i}}\,(\lambda (x :
\U_{\castOfPi{i}}).\uU_{\castOfPi{i}})$ when $\castOfPi{i} \geq 0$,
and its decoding to types
$\stalkCIC{i}{h} := \El\,(\stalkCode{i}{h})$.
The unknown type $\unkU[i]$ is then decoded to the extended dependent sum
$\liftSigma \, \C_i \, \stalkCIC{i}{}$ whose elements are

* one of the two freely added constructors $\lifttop{\liftSigma},
\liftbot{\liftSigma}$ following the interpretation scheme of inductive types;

* or a dependent pair $\pairSigma{h}{t}$ of a head constructor $h \in \H_i$
together with an element $t \in \stalkCIC{i}{h}$.

Finally, the error type $\errU[i]$ is decoded to the unit type $\unit$ containing a unique element

A ∈_i
B ∈  A →_j A B
∈_ij j < i_j ∈_i ∈_i [i] ∈_i [i] ∈_i

\begin{align*}
\El\,(\PiU\,A\,B) &= \Pi(a : \El\,A)~\El (B\,a)
& \El\,\uU_j &= \U_j
& \El\,\natU &= \liftNat{}
& \El\,\unkU[i] &= \liftSigma \, \C_i \, \stalkCIC{i}{}
& \El\,\errU[i] &= \unit
\end{align*}

[IR universe     exceptions]Inductive-recursive encoding of the
discrete universe hierarchy

Variants of
Crucially, the code for $\Pi$-types (<ref>) depends on the choice made for $\sortOfPi{i}{j}$.

Observe that for the choice of parameters corresponding to , the
inductive-recursive definition of $\U_i$ is ill-founded since
$\castOfPi{\sortOfPi{i}{i}} = \sortOfPi{i}{i}$. We can thus inject
$\stalk{}_{\sortOfPi{i}{i}}\Pi = \El\,\unkU{\sortOfPi{i}{i}} \to
\El\,\unkU{\sortOfPi{i}{i}}$ into $\El\,\unkU{\sortOfPi{i}{i}}$ and project
back in the other direction, exhibiting an embedding-retraction
suitable to interpret the untyped $\lambda$-calculus and hence $\Omega$.
[In the  implementation, we deactivate the termination checker
on the definition of the universe for the model interpreting ,
thus effectively working in a partial, inconsistent type theory.]

In order to maintain normalization, the construction of the unknown type and the
universe therefore needs to be stratified, which is possible when
$\castOfPi{\sortOfPi{i}{i}} < \sortOfPi{i}{i}$.

This strict inequality occurs for both and .

We then proceed by strong induction on the universe level, and note that thanks to
the level gap, the decoding $\El\,\unkU[i]$ of the unknown type at a level $i$
can be defined solely from the data of smaller universes available by inductive
hypothesis, without any reference to $\U_i$.

We can then define the rest of the universe $\U_i$ and the decoding function
$\El$ at level $i$ in a well-founded manner, validating the strict positivity
criterion of 's termination checker.

\begin{align*}
\?_{\PiU{}\,A\,B} &:= \l x : \El\,A. \?_{\El\,(B\,x)}
& \?_{\uU_j} &:= \unkU[j]
&\?_{\natU} &:= \lifttop{\liftNat}
& \?_{\unkU[j]} &:= \lifttop{\El\,\uU_j}
& \?_{\errU[j]} &:= \unitK
\\
\err_{\PiU{}\,A\,B} &:= \l x : \El\,A. \err_{\El\,(B\,x)}
& \err_{\uU_j} &:= \errU[j]
&\err_{\natU} &:= \liftbot{\liftNat}
&\err_{\unkU[j]} &:= \liftbot{\El\,\uU_j}
& \err_{\errU[j]} &:= \unitK
\end{align*}

Realization of exceptions

The definition of exceptions $\?_{A}, \err_{A} : \El~A$ at an arbitrary code $A$ then
follows by case analysis on the code, as shown in <ref>.

On the code for the universe, $\uU_j$, we directly use the code for the unknown and the error
types respectively.

On codes that have an inductive interpretation—$\natU$,
$\unkU[i]$—we use the two added constructors.

On the code for dependent functions, exceptions are defined by re-raising the exception at the
codomain in a pointwise fashion.

Finally, on the error type $\errU$, exceptions are degenerated and
forced to take the only value $\unitK:\unit$[This definition is indeed uniform if
$\unit$ is seen as the record type with no projection.] of its interpretation as a

\[
\begin{array}[t]{lcl}
\cas~(\PiU\,A^\pidom\,A^\picod)~(\PiU\,B^\pidom\,B^\picod)~f & := & \l b :
\El\,B^\pidom.~\letin{a}{\cas~B^\pidom~A^\pidom~b}{\cas\,
(A^\picod\,a)~(B^\picod\,b)~(f\,a)} \\
\cas~(\PiU\,A^\pidom\,A^\picod)~\unkU[i]~f & := & (\Pi ;
\cas~(\PiU\,A^\pidom\,A^\picod)~(\stalkCode{i}{\Pi})~f)\qquad
\text{if }
\stalkCode{i}{\Pi} \neq \errU\\
\cas~(\PiU\,A^\pidom\,A^\picod)~X~f & := & \err_X \qquad \text{otherwise}
\end{array}
\]

\[
\hspace{1cm}\begin{array}[t]{lcl}
\cas~\natU~\natU~n &:=& n\\
\cas~\natU~\unkU[i]~n &:=& (\nat; n)\\
\cas~\natU~X~n &:=& \err_X\\[0.3cm]

\cas~\errU[i]~Z~\unitK &:=& \err_Z\\
\\
\\
\end{array}%
\hspace{1cm}%
\begin{array}[t]{lcl}
\cas~\uU_j~\uU_j~A & := & A \\
\cas~\uU_j~\unkU[i]~A & := & (\square_j ; A) \qquad \text{if } j < i\\
\cas~\uU_j~X~A & := & \err_X \qquad \text{otherwise}\\[0.3cm]
\cas~\unkU[i]~Z~(c ; x) & := & \cas~(\stalkCode{i}{c})~Z~x\\
\cas~\unkU[i]~Z~\lifttop{\El\,\unkU[i]} & := & \?_Z\\
\cas~\unkU[i]~Z~\liftbot{\El\,\unkU[i]} & := & \err_Z\\
\end{array}
\]

Definition of $\cas$ (discrete model)

Equipped with exceptions and type analysis, we define
induction on the universe levels and case analysis on the codes of the types
$A$ and $B$ (<ref>).

In the total setting (when $\castOfPi{\sortOfPi{i}{i}} < \sortOfPi{i}{i}$), the definition of $\cas$ is well-founded: each recursive
call happens either at a strictly smaller universe (the two cases for
$\PiU$) or on a strict subterm of the term being cast (case of
inductives,  $\natU$ and $\unkU$).

Note that each of the defining equations of $\cas$ corresponds straightforwardly to a
reduction rule of <ref>.

Discrete translation

We can finally define the discrete syntactic model of in (<ref>).
The translations $\bareTm{-}$ and $\bareTy{-}$ are defined by induction on the syntax of
terms and types.

A type $A$ is translated to its corresponding code $\bareTm{A}$
in $\U_i$ when seen as a term, and is translated to the interpretation
of this code $\bareTy{A} := \El\,\bareTm{A}$ when seen as a type.

$\?_A$ and $\err_A$ are directly translated using the exceptions
defined in <ref>.

The following theorem shows that the translation is a syntactic model in the sense
of <cit.>.

\[
\begin{array}[t]{lcl}
\bareTy{\cdot} & := & \cdot\\[0.6em]
\bareTy{A} & := & \El\,\bareTm{A} \\
\\
{\bareTm{ x }} & := & x\\
{\bareTm{\square{}_i}} & := & \uU_i \\[0.6em]
{\bareTm{\P x : A . B}} & := & \PiU~\bareTm{ A }~(\l x : \bareTy{A} . \bareTm{ B }) \\
{\bareTm{t~u}} & := & \bareTm{t}~\bareTm{u}\\
{\bareTm{\l x : A . t}} & := & \l x : \bareTy{ A } . \bareTm{t}
\end{array}%
\begin{array}[t]{lcl}
\bareTy{\Gamma, x : A} & := & \bareTy{\Gamma}, x : \bareTy{A}\\[0.6em]
{\bareTm{\nat}} & := & \natU \\
{\bareTm{0}} &:= & 0\\
{\bareTm{\suc}} & := & \suc \\
\bareTm{\ind_{\nat}}~ P~h_0\,h_{\suc} & :=& \ind_{\liftNat{}}~P~h_0\,h_{\suc}\,\?_{P\,\?_{\liftNat{}}}\,\err_{(P\err_{\liftNat{}})} \\[0.6em]
{\bareTm{\?_A}} & := & \?_{\bareTm{A}}\\
{\bareTm{\err_A}} &:= & \err_{\bareTm{A}} \\
{\bareTm{ \ascdom{t}{A}{B} }} &:= & \cas\,\bareTm{A}\,\bareTm{B}\,\bareTm{t}
\end{array}
\]

Discrete translation from to

The translation defined in <ref>
preserves conversion and typing derivations:

* if $\tcol{\Gamma} \caty \tcol{t} \redCCIC{} \tcol{u}$ then $\bareTy{\Gamma} \irty \bareTm{t}
\redIRn \bareTm{u}$, in particular $\bareTy{\Gamma} \irty \bareTm{t}
\equiv \bareTm{u}$,

* if $\tcol{\Gamma} \caty \tcol{t} : \tcol{A}$ then $\bareTy{\Gamma} \irty \bareTm{t} : \bareTy{A}$.

(1) All reduction rules from are preserved without a
change so that we only need to be concerned with the reduction rules involving
exceptions or casts.

A careful inspection shows that these reductions are preserved too once we
observe that the terms of the shape
$\tcol{\ascdom{t}{\stalkCIC{i}{h}}{\?_{\square_i}}}$ that are stuck in are in one-to-one correspondence with the one-step reduced form of its
translation $\pairSigma{h}{\bareTm{t}} : \liftSigma \, \H_i \,
\stalkCIC{i}{}$.

(2) Proved by a direct induction on the typing derivation of
$\catyJ{\Gamma}{t}{A}$, using the fact that exceptions and casts are well-typed—that is $\irty \? : \P(A : \U_i)\,\El\,A$ , $\irty \err : \P(A : \U_i)\,\El\,A$, and $\irty \cas : \P(A : \U_i)(B : \U_i)
\El\,A {\to} \El\,B$—and relying on assertion $(1)$ to handle the
conversion rule.

As explained in <ref>, <ref>
implies in particular that and are strongly

§.§ Poset-Based Models of Dependent Type Theory

The simplicity of the discrete model comes at the price of an inherent inability to
characterize which casts are guaranteed to succeed, a graduality theorem.

To overcome this limitation, we develop a monotone model on top of the discrete
model where, by construction, each type $A$ comes equipped with an order
structure $\sqsubseteq^A$—a reflexive, transitive, antisymmetric and
proof-irrelevant relation—modelling precision between terms.

In particular, the exceptions $\err_A$ and $\?_A$ correspond respectively to the smallest
and greatest element of $A$ for this order.

We note  for a universe of types equipped with the structure of a poset
together with smallest and greatest elements.

Each term and type constructor is enforced to be monotone with respect to these orders,
providing a strong form of graduality.

This implies in particular that such a model cannot be defined for because this type theory lacks graduality, as shown by <ref>.

As an illustration, the order on extended natural numbers (<ref>) makes
$\liftbot{\liftNat}$ the smallest element and $\lifttop{\liftNat}$ the biggest element.[We abusively note $\liftNat$ for both
the poset and its carrier to avoid introducing too many notations.]

The standard natural numbers – $\natzero$ or $\natsuc~n$ for a standard natural
number $n$ – then stand between failure and indeterminacy,
but are never related to each other by precision. Indeed, in order to ensure conservativity with respect to , $\sqsubseteq^{\natU{}}$ must coincide with 's conversion on static closed natural numbers.

\begin{align*}
0 &\sqsubseteq^{\natU} 0
&\liftbot{\liftNat} &\sqsubseteq^{\natU} n\\
0 &\sqsubseteq ^{{\natU}} \lifttop{\liftNat}
&\lifttop{\liftNat} &\sqsubseteq^{{\natU}} \lifttop{\liftNat}
\end{align*}

n ⊑^ m n ⊑^  m n ⊑^  n ⊑^

Order structure on extended natural numbers

Beyond the precision order on types, the nature of dependency forces us to spell
out what the precision between types entails.

Following the analysis of <cit.>,
a relation $A \sqsubseteq B$ between types should
induce an embedding-projection pair (): a pair of an upcast
${\upcast{} : A {\to} B}$ and a downcast ${\downcast{} : B {\to} A}$
satisfying a handful of properties with gradual guarantees as a

An  $d : A \distr{} B$ between posets $A,B : \poset$ consists of

* an underlying relation $d \subseteq A \times B$ such that

\[a' \sqsubseteq^A a \>\wedge\> d(a,b) \>\wedge\> b \sqsubseteq^B b' \quad\implies\quad d(a',b')\]

* that is bi-represented by $\upcast_d~ : A \to B$, $\downcast{}_d : B \to
\[\upcast_d a \sqsubseteq^B b \quad\Leftrightarrow\quad d(a,b) \quad\Leftrightarrow\quad a \sqsubseteq^A \;\downcast_d b,\]

* such that the equality $\downcast_d \circ \upcast_d~ = \id_A$ holds.

Note that here equiprecision of the retraction becomes an equality
because of antisymmetry.

Under these conditions, $\upcast_d : A \hookrightarrow B$ is injective,
$\downcast_d : B \twoheadrightarrow A$ is surjective and both preserve bottom
elements, explaining that we call $d : A \distr{} B$ an embedding-projection

The definition of  is based on a relation rather than just its
pair of representing functions to highlight the connection between  and
parametricity <cit.>.

Assuming function extensionality, being an  is a
property of the underlying relation: there is at most one pair $(\upcast{}_d,
\downcast_d)$ representing the underlying relation of $d$.

An  straightforwardly induces the following
relations that will be used in later proofs.

Let $d : A \distr{} B$ be an  between posets.

* If $a : A$ then $d\,(a, \upcast_d a)$ and $a \sqsubseteq^A
\downcast_d\upcast_d a$.

* If $b : B$ then $d\,(\downcast_d b, b)$ and $\upcast_d\downcast_d b \sqsubseteq^B

Posetal families
By monotonicity, a family $B : A \to \poset$ over a poset $A$ gives rise not
only to a poset $B\,a$ for each $a \in A$, but also to  $B_{a,a'} :
B\,a \distr{} B\,a'$ for each $a \sqsubseteq^A a'$.
These  need to satisfy functoriality conditions:

\[B_{a,a} = {\sqsubseteq^{B\,a}} \qquad\text{and}\qquad B_{a,a''} = B_{a',a''}
\circ B_{a,a'}\quad \text{whenever}\quad a \sqsubseteq^A a' \sqsubseteq^A
In particular, this ensures that heterogeneous transitivity is well

\[B_{a,a'}(b,b') \wedge B_{a',a''}(b',b'') \Rightarrow

Dependent products
Given a poset $A$ and a posetal family $B$ over $A$, we can form the poset
$\Pmon{}\,A\,B$ of monotone dependent functions from $A$ to $B$,
equipped with the pointwise order.

Its inhabitants are dependent functions $f : \P (a : A). B\,a$ such that $a \sqsubseteq^A
a' {\Rightarrow} B_{a,a'}\,(f\,a, f\,a')$.

Moreover, given  $d_A : A \distr{} A'$ and $d_B : B \distr{} B'$, we
can build an induced  $d_\Pi : \Pmon{}\,A\,B \distr{} \Pmon{}\,A'\,B'$
with underlying relation

\begin{align*}
d_\Pi(f,f') &:= d_A(a,a') \Rightarrow d_B(f\,a,f'\,a'),\\
\upcast{}_{d_\Pi}f := {\upcast_{d_B}}\circ f \circ \downcast{}_{d_A}
&\qquad\text{ and }\qquad
\downcast{}_{d_\Pi}f := {\downcast_{d_B}} \circ f \circ \upcast{}_{d_A}.
\end{align*}

The general case where $B$ and $B'$ actually depend on $A, A'$ is obtained with
similar formulas, but a larger amount of data is required to handle
the dependency: we refer to the accompanying  development for details.

Inductive types

Generalizing the case of natural numbers, the order on an arbitrary extended
inductive type $\liftErr{I}$ uses the following scheme:

* $\liftbot{\liftErr{I}}$ is the least element

* $\lifttop{\liftErr{I}} \sqsubseteq^{\liftErr{I}} \lifttop{\liftErr{I}}$

* $c~\mathbf{t} \sqsubseteq^{\liftErr{I}} \lifttop{\liftErr{I}}$ whenever $t_i \sqsubseteq^{X_i} \lifttop{X_i}$ for
all $i$

* each constructor $c$ is monotone with respect to the order on its arguments

The precondition on subterms in the third case is unnecessary in simple cases
and is kept to be uniform with definition of order on the monotone unknown type
in the following section.

Similarly to dependent product, an  $\mathbf{X} \distr{} \mathbf{X'}$
between the parameters of an extended inductive type $\liftErr{I}$ induces an
$\liftErr{I}\,\mathbf{X} \distr{} \liftErr{I}\,\mathbf{X'}$.

For instance,  $d_A : A \distr{} A'$ and $d_B : B \distr{} B'$ induce
an  $d_{\liftSigma} : \liftSigma\,A\,B \distr{} \liftSigma\,A'\,B'$
defined by $d_{\liftSigma}((a,b),(a',b')) := d_A(a,a') \wedge d_B(b,b')$.

§.§ Microcosm: the Monotone Unknown Type

The interpretation [i] of the unknown type in the monotone model should
morally group together approximations of every type at the same universe

Working in (bi)pointed orders, [i] can be realized as a coalesced sum
<cit.> of
the family $\stalkCIC{i}{h}$ indexed by head constructors $h \in \H_i$.

A concrete presentation of [i] is obtained as
the quotient of $\liftSigma\, \H_i \, \stalkCIC{i}{}$
identifying $\liftbot{\liftSigma\, \H_i \, \stalkCIC{i}{}}$ with any pair

The equivalence classes of $\pairSigma{h}{x}$ is noted as $\unkInj{h}{x}$,
$\liftbot{\liftSigma\, \H_i \, \stalkCIC{i}{}}$ as $\liftbot{\unkMon[i]}$ and
$\lifttop{\liftSigma\, \H_i \, \stalkCIC{i}{}}$ as $\lifttop{\unkMon[i]}$.

The obtained type [i] is then equipped
with a precision relation defined by the rules:

\begin{align}
\label{eq:unknown-prec}
\liftbot{\unkMon[i]} &\sqsubseteq^{\unkU[i]} z
& \lifttop{\unkMon[i]} &\sqsubseteq^{\unkU[i]} \lifttop{\unkMon[i]}
& \inferrule{x \sqsubseteq^{\stalkCode{i}{h}} x'}{ \unkInj{h}{x} \sqsubseteq^{\unkU[i]} \unkInj{h}{x'}} &
& \inferrule{}%{x \sqsubseteq^{\stalkCode{i}{h}} \?_{\stalkCode{i}{h}}}
{\unkInj{h}{x} \sqsubseteq^{\unkU[i]} \lifttop{\unkMon[i]}}
\end{align}

These rules ensure that the exceptions
$\liftbot{\unkMon[i]}$ and $\lifttop{\unkMon[i]}$ are
respectively the smallest and biggest elements of $\unkMon[i]$.

Non-exceptional elements
are comparable only if they have the same head constructor $h$ and if so are
compared according to the interpretation of that head constructor as an ordered
type $\stalkCIC{i}{h}$ .

Because of the quotient, it is not immediate that this presentation of
$\sqsubseteq^{\unkMon[i]}$ is independent of the choice of representatives in
equivalence classes and that it forms a proof-irrelevant relation.

In the formal development, we define the relation by quotient-induction on each argument, thus verifying that it respects the quotient, and also show that
it is irrelevant. This relies crucially on equality being decidable
on head constructors when comparing $\unkInj{h}{x}$ and $\unkInj{h'}{x'}$.

In order to globally satisfy $\pgrad$, [i] should admit an  ${d_h
: \stalkCIC{i}{h} \distr{} \unkMon[i]}$ whenever we have a head constructor $h
\in \H_i$ such that $\stalkCode{i}{h} \sqsubseteq \unkU[i]$ (we return to that
point in the next section <ref>).

Embedding an element $x \in \stalkCIC{i}{h}$ by $\upcast_{d_h}x = \unkInj{h}{x}$
and projecting out of $\stalkCIC{i}{h}$ by the following equations form a reasonable

\begin{align*}
\downcast_{d_h}\unkInj{h'}{x} &=
\begin{dcases*}
x & if $h = h'$ \\
\err_{\stalkCIC{i}{h}} & otherwise
\end{dcases*}&
\downcast_{d_h} \lifttop{\unkMon[i]} &= \?_{\stalkCIC{i}{h}} &
\downcast_{d_h} \liftbot{\unkMon[i]} &= \err_{\stalkCIC{i}{h}}
\end{align*}

Note that we rely again on $\H$ having decidable equality to compute the
Moreover $_d_h ⊣_d_h$ should be adjoints; in particular,
the following precision relation needs to hold:
\begin{align*}
\err_{\stalkCIC{i}{h}} \sqsubseteq^{\stalkCIC{i}{h}} {\downcast{}_{d_h}\liftbot{\unkMon[i]}}\quad \iff \quad
\unkInj{h}{\err_{\stalkCIC{i}{h}}} = {\upcast_{d_h}\err_{\stalkCIC{i}{h}}} \sqsubseteq^{\unkMon[i]} \liftbot{\unkMon[i]}
\end{align*}
Since $⊑^[i]$ should be antisymmetric, this is possible only
if $h_ih$ and $[i]$ are
identified in $[i]$, explaining why we have to quotient in the first place.

\subsection{Realization of the Monotone Universe Hierarchy}
\label{sec:monotone-universe}

\begin{figure}
\begin{small}
\begin{center}
\textbf{Monotone universes} $\U_i$
\textbf{and decoding function}  $\El\, : \U_i \to \poset$
\text{(cases distinct from \cref{fig:discrete-univ})}
\end{center}
\vspace{0.5em}
\begin{minipage}{0.40\linewidth}
\[
\inferrule{A \in \U_i\\ B \in \Pmon(a :\El\, A).\,\U_j}{\PiU\,A\,B \in \U_{\sortOfPi{i}{j}}}
\]
\end{minipage}%
\begin{minipage}{0.60\linewidth}
\begin{align*}
\El\,(\PiU\,A\,B) &= \Pmon (a : \El\,A).\, \El (B\,a)
& \El\,\unkU[i] &= \unkMon[i]
\end{align*}
\end{minipage}
\vspace{1em}
\begin{center}
\textbf{Precision order} $\sqsubseteq$ \textbf{on the universes}
(where $i \le j$)
\end{center}
\vspace{0.5em}
\begin{mathpar}
\inferrule[$\errU$-$\sqsubseteq$]{A : \U_j }{\Ue{\errU[i]}{A}}
\and
\inferrule[$\natU$-$\sqsubseteq{}$]{ }{\Ue{\natU}{\natU}}
\and
\inferrule[$\uU$-$\sqsubseteq$]{ }{\Ue{\uU_i}{\uU_{i}}}
\and
\inferrule[$\unkU$-$\sqsubseteq$]{ }{\Ue{\unkU[i]}{~\unkU[j]}}
\and
\inferrule[$\PiU$-$\sqsubseteq$]{\Ue{A}{A'}\\ a:\El\,A,a':\El\,A', a_\epsilon : a
\precision{A}{A'} a' \vdash \Ue{B\,a}{B'\,a'}}
\and
\inferrule[$\C$-$\sqsubseteq$]{h = \hd{A} \in \C_i\\\Ue{A}{\stalkCode{j}{h}}}{\Ue{A}{~\unkU[j]}}
\end{mathpar}
\vspace{1em}
\begin{center}
\textbf{Precision on terms} $\precision{A}{B} := \ElRel(A{\sqsubseteq}B)$
\end{center}
\vspace{0.5em}
\begin{mathpar}
% rule corresponding to [$\errU$-$\sqsubseteq$]
\inferrule[$\ElRel(\errU\text{-}{\sqsubseteq})$]{a:\El~A}{\unitK \precision{\errU}{A} a}
\and
% rule corresponding to [$\natU$-$\sqsubseteq{}$] and [$\uU$-$\sqsubseteq$]
\inferrule[$\ElRel(\natU\text{-}{\sqsubseteq}),\ElRel(\uU\text{-}\sqsubseteq)$]
{A = \natU, \uU_{i}\\ x \sqsubseteq^{\El~A} y}{x \precision{A}{A} y}
\and
% rules corresponding to [$\unkU$-$\sqsubseteq$]
% there are some redondances, the first rule is derivable from the 2 others
% (and not uniquely)
\inferrule[$\ElRel(\unkU\text{-}{\sqsubseteq})$]{z : \unkMon[j]}{\err_{\unkU[i]} \precision{\unkU[i]}{\unkU[j]} z}
\and
\inferrule{z : \unkMon[i]}{ z \precision{\unkU[i]}{\unkU[j]} \?_{\unkU[j]}}
\and
\inferrule{x \precision{\stalkCode{i}{h}}{\stalkCode{j}{h}} x'}{\unkInj{h}{x} \precision{\unkU[i]}{\unkU[j]} \unkInj{h}{x'}}
\and
% rule corresponding to [$\PiU$-$\sqsubseteq$]
\inferrule[$\ElRel(\PiU\text{-}{\sqsubseteq})$]{a:\El\,A,a':\El\,A', a_\epsilon : a \precision{A}{A'} a' \vdash
f~a \precision{B\,a}{B'\,a'}f'~a'}
{f \precision{\PiU\,A\,B}{\PiU\,A'\,B'} f'}
\and
% rules corresponding to [$\C$-$\sqsubseteq$]
\inferrule[$\ElRel(\C\text{-}{\sqsubseteq})$]{a \precision{A}{\stalkCode{j}{(\hd{A})}} x}{a \precision{A}{\unkU[j]} \unkInj{\hd{A}}{x}}
\and
\inferrule{a:\El~A}{a \precision{A}{\unkU[j]} \?_{\unkU[j]}}
% \and
% \inferrule{z: \unkMon[j]}{\err_A \precision{A}{\unkU[j]} z}
% This rule is not needed (it can be derived by err_A \sqsubseteq [head A;
% err_A ] = err_? \sqsubseteq z )
\end{mathpar}
\end{small}
\caption{Monotone universe of codes and precision}
\label{fig:IRUniverse}
\end{figure}

Following the discrete model, the monotone universe hierarchy is
also implemented through an inductive-recursive datatype of codes $_i$
together with a decoding function $: _i →□$, both presented in
\cref{fig:IRUniverse}.
The precision relation $⊑ : _i →_j →□$
presented below is an
order (\cref{thm:universe-hierarchy}) on this universe hierarchy.
The ``diagonal'' inference rules, providing evidence for relating type
constructors from \CIC, coincide with those of binary
Outside the diagonal, $$ is placed at the bottom.
More interestingly, the derivation of a precision proof $A ⊑$ provides a unique decomposition of $A$ through iterated germs
directed by the relevant head constructors.
For instance, in the gradual systems \CCICP and \CCICs where the equation $ij =
max(i,j)$ holds for any universe levels $i,j$, the derivation of $( → ) →
⊑$ canonically decomposes as:
\[ (\natU{} {\to} \natU{}) {\to} \natU{} \quad \sqsubseteq
\quad (\unkU {\to} \unkU) {\to} \natU{} \quad \sqsubseteq
\quad \unkU {\to} \unkU \quad \sqsubseteq\quad \unkU\]

This unique decomposition is at the heart of the reduction of the cast
operator given in~\cref{fig:CCIC-reduction}, and it can be described informally
as taking the path of maximal length between two related types.\footnote{This
decomposition is already present in~\cite{newAhmed:icfp2018} and
to be contrasted with the AGT approach~\cite{garciaAl:popl2016}, which tends
to pair a value with the most precise witness of its type, \ie~canonical path of minimal length.}
Such a derivation of precision $A ⊑B$ gives rise through decoding to
\eppairs{} $ (A ⊑B) :  A  B$, with underlying relation
noted $AB :  A → B →□$.
This decoding function $$ is described on generators of $⊑$ at
the bottom of~\cref{fig:IRUniverse}.
$(-⊑)$ states that the unique value $$ of
$ = $ is smaller than any other value.
The diagonal cases
$(-⊑)$ and $(-⊑)$ reuse
the order specified on the carrier.
The \eppair $(-⊑)$ between two unknown types
$[i]  [j]$ at potentially distinct universe levels $i ≤j$ stipulate that $_[i]$ and $_[j]$ are respectively smaller
and greater than any other value, and that the comparison between two injected
terms with same head is induced by their second component.
Note that these rules are redundant since $$ is obtained through a quotient.
Functions $f,f'$ are related by $(-⊑)$ when they map
related elements $a AA' a'$ to related elements $f a B aB' a'f' a'$.
Finally, $(-⊑)$ embeds a type
$A$ into $$ through its $$.

It is interesting to observe what happens in \CCICT,
$ij ≠max(i,j)$, for instance on the previous example:
\[\natU{} {\to} \natU{} \quad \not\sqsubseteq \quad \errU =
\stalkCode{0}{\Pi} \quad \sqsubseteq \quad \unkU \]
So $ → $ is not lower than $$ in that setting.

One crucial point of the monotone model is the mutual definition of codes $_i$
together with the precision relation, particularly salient on codes for
$Π$-types: in $ A B$, $B :  A →_i$ is a monotone function with
respect to the order on $ A$ and the precision on $_i$.
This intertwining happens because the order is required to be reflexive, a fact
observed previously by~\citet{AtkeyGJ14} in the similar setting of reflexive
Indeed, a dependent function $ f : Π(a :  A).    (B a)$ is related to
itself $f  A B A B f$ if and only if $f$ is
\emph{monotone}.

\begin{theorem}[Properties of the universe hierarchy]\text{}
\label{thm:universe-hierarchy}
\begin{enumerate}
\item $\sqsubseteq$ is reflexive, transitive, antisymmetric and irrelevant so
that $(\U_i, \sqsubseteq)$ is a poset.
\item $\U_i$ has a bottom element $\errU[i]$ and a top element $\unkU[i]$; in
particular, $A \sqsubseteq \unkU[i]$ for any $A : \U_i$.
\item $\El : \U_i \to \square$ is a family of posets over $\U_i$ with underlying relation
$\precision{A}{B}$ whenever $A \sqsubseteq B$.
\item $\U_i$ and $\El\;A$ for any $A : \U_i$ verify UIP\footnote{Uniqueness of
Identity Proofs; in HoTT parlance, $\U_i$ and $\El\,A$ are hSets.}: the equality on these
types is irrelevant.
\end{enumerate}
\end{theorem}
\begin{proof}[Proof sketch]
All these properties are proved mutually, first by strong induction on the
universe levels, then by induction on the codes of the universe or the
derivation of precision. Here, we only sketch the proof of point $(1)$ and refer to the Agda
development (\cf \texttt{UnivPartial.agda}) for detailed formal proofs.

For reflexivity, all cases are immediate but for $\PiU\,A\,B$: the induction
hypothesis provides $A \sqsubseteq A$ and by point $(3)$ $\ElRel{}(A
\sqsubseteq A) = {\sqsubseteq^A}$ so we can apply the monotonicity of $B$.

For anti-symmetry, assuming $A \sqsubseteq B$ and $B \sqsubseteq A$, we prove
by induction on the derivation of $A \sqsubseteq B$ and case analysis on the other
derivation that $A \equiv B$. Note that we never need to consider the rule
$\C$-$\sqsubseteq$. The case $\Pi$-$\sqsubseteq$ holds by induction hypothesis
and because the relation ${}_A\sqsubseteq_A$ is reflexive. All the other cases
follow from antisymmetry of the order on universe levels.

For transitivity, assuming $AB : A \sqsubseteq B$ and $BC : B
\sqsubseteq C$, we prove by induction on the (lexicographic) pair $(AB,BC)$
that $A \sqsubseteq C$:
\begin{description}
\item[Case $AB = \unkU\dash{\sqsubseteq}$,] necessarily $BC =
\unkU\dash{\sqsubseteq}$, we conclude by $\unkU\dash{\sqsubseteq}$.
\item[Case $AB = \C\dash{\sqsubseteq}$,] necessarily $BC =
\unkU\dash{\sqsubseteq} , \unkU[j] \sqsubseteq \unkU[j']$, we can
thus apply the inductive hypothesis to
${A \sqsubseteq \stalkCode{j}{(\hd{A})}}$ and
${\stalkCode{j}{(\hd{A})} \sqsubseteq \stalkCode{j}{(\hd{A})}}$
in order to conclude with $\C\dash{\sqsubseteq}$.
\item[Case $AB = \errU\dash{\sqsubseteq}$,] we conclude immediately by $\errU\dash{\sqsubseteq}$.
\item[Case $AB = \natU\dash{\sqsubseteq}, BC = \natU\dash{\sqsubseteq}$] we
conclude with $\natU\dash{\sqsubseteq}$.
\item[Case $AB = \uU\dash{\sqsubseteq}, BC = \uU\dash{\sqsubseteq}$] immediate
by $\uU\dash{\sqsubseteq}$.
\item[Case $AB = \PiU\dash{\sqsubseteq}, BC = \PiU\dash{\sqsubseteq}$]
by hypothesis we have
\begin{mathpar}
A = \PiU\,A^\pidom\,A^\picod \and
B = \PiU\,B^\pidom\,B^\picod \and
C = \PiU\,C^\pidom\,C^\picod \and
A^\pidom \sqsubseteq B^\pidom \and
B^\pidom \sqsubseteq C^\pidom \and
AB^\picod : \forall a\,b, a \precision{A^\pidom}{B^\pidom} b \to A^\picod\,a \sqsubseteq B^\picod\,b \and
BC^\picod : \forall b\,c, b \precision{B^\pidom}{C^\pidom} c \to B^\picod\,b \sqsubseteq C^\picod\,c
\end{mathpar}
By induction hypothesis applied to $A^\pidom \sqsubseteq B^\pidom$ and
$B^\pidom \sqsubseteq C^\pidom$, the domains of the dependent product are related $A^\pidom \sqsubseteq C^\pidom$.
For the codomains, we need to show that for any $a : A^\pidom, c : C^\pidom$
such that $a \precision{A^\pidom}{C^\pidom} c$ we have
$A^\picod\,a \sqsubseteq C^\picod\,c$. By induction hypothesis, it is enough to prove that
$A^\picod\,a \sqsubseteq B^\picod\,(\upcast_{A^\pidom\sqsubseteq B^\pidom}a)$
and $B^\picod\,(\upcast_{A^\pidom\sqsubseteq B^\pidom}a) \sqsubseteq
The former follows from $AB^\picod$ applied to
$ a \precision{A^\pidom}{B^\pidom} \upcast_{A^\pidom\sqsubseteq B^\pidom} a
\Leftrightarrow a \sqsubseteq^{A^\pidom} { \downcast{} }{ \upcast{} } a \Leftrightarrow a \sqsubseteq^{A^\pidom} a$ which holds by reflexivity, and the latter
follows from $BC^\picod$ applied to $\upcast_{A^\pidom\sqsubseteq B^\pidom}
a \precision{B^\pidom}{C^\pidom} c \Leftrightarrow a \precision{A^\pidom}{C^\pidom} c$.
\item[Otherwise,]
we are left with the cases where $AB = \natU\dash{\sqsubseteq},
\PiU\dash{\sqsubseteq}$ or $\uU\dash{\sqsubseteq}$ and
$BC = \C\dash{\sqsubseteq}$, we apply the inductive hypothesis to
$AB$ and $B \sqsubseteq \stalkCode{j}{(\hd{B})}$ in order to conclude
with $\C\dash{\sqsubseteq}$.
\end{description}
% So $\sqsubseteq$ is a reflexive, transitive and antisymmetric relation,
Finally, we show proof-irrelevance, \ie~that for any $A,B$ there is at most one
derivation of $A \sqsubseteq B$. Since the conclusions of the rules do not
overlap, we only have to prove that the premises of each rules are uniquely
determined by the conclusion. This is immediate for $\PiU\dash{\sqsubseteq}$.
For $\C\dash{\sqsubseteq}$, $h = \hd{A} \in \C_i$ with $i = \pred\,j$ are uniquely
determined by the conclusion so it holds too.
\end{proof}

\subsection{Monotone Model of \CCICs}
\label{sec:monotone-model}

The monotone translation $-$ presented in \cref{fig:monotone-translation} brings together the monotone
interpretation of inductive types (e.g. $$), dependent products, the unknown type
$$ as well as the universe hierarchy.
Following the approach of~\citet{newAhmed:icfp2018}, casts are derived out of the
canonical decomposition through the unknown type using the property $(2)$
\[\monTm{\ascdom{t}{A}{B}} \quad:= \quad\downcast{}_{\raisebox{-2pt}{\tiny$\ElRel{\monTm{B}{\sqsubseteq}\unkU}$}}\upcast_{\raisebox{-2pt}{\tiny$\ElRel{\monTm{A}{\sqsubseteq}\unkU}$}}\monTm{t} \]
Note that this definition formally depends on a chosen universe level $j$ for
$: _j$, but the resulting operation is independent of this choice thanks to the
section-retraction properties of \eppairs{}.
The difficult part of the model, the monotonicity of $$, thus holds by design.
However, the translation of some terms do not reduce as in \CCIC{}: $$ can
get stuck on type variables eagerly, \eg on a \nameref{redrule:down-err}
step.\footnote{An analysis of the correspondence between the discrete and
monotone models can be found in \cref{sec:logical-relation}.}
These reduction rules still hold propositionally though so that we have at least
a model in an extensional variant of the target theory (\ie~in which two terms
are \emph{definitionally} equal whenever they are \emph{propositionally} so).
\begin{lemma}
If $\tcol{\Gamma} \caty \tcol{t} \redCCIC{} \tcol{u}$ then there exists a \CICIRQ
term $e$ such that
$\monTm{\Gamma} \irty e : \monTm{t} = \monTm{u}$.
\end{lemma}
We can further enhance this result using the fact that we assume
functional extensionality in our target and can prove that the translation of
all our types satisfy \UIP{}.
Under these assumptions, the conservativity results
of~\citet{Hofmann95} and \citet{WinterhalterST19} apply, so we can recover a translation
targeting \CICIRQ.
\begin{theorem}[Monotone model]
\label{thm:monotone-model}
The translation $\monTm{-}$ of \cref{fig:monotone-translation} extends to a
model of \CCIC into \CIC extended with induction-recursion and functional
extensionality: if $\catyJ{\Gamma}{t}{A}$ then $\monTy{\Gamma}
\irty \monTm{t} : \monTy{A}$.
\end{theorem}
It is unlikely that the principle that we demand in the target calculus $$ are optimal.
We conjecture that a variation of the translation described here could be
developed in \CIC{} extended only with induction-induction to describe the
intensional content of the codes $$ in the universe, and strict
propositions~\cite{GilbertCST19} following the construction of the setoid models of
type theory~\cite{Altenkirch99,AltenkirchBKT19,AltenkirchBKSS21}.

\begin{figure}
\begin{small}
\begin{center}
\textbf{Monotone translation of contexts}
\end{center}
\[
\vspace{0.5em}
\begin{array}[t]{lcl}
\monTy{\cdot} & := & \cdot\\
\monTyRel{\cdot} & := & \cdot\\
\end{array}\qquad%
\begin{array}[t]{lcl}
\monTy{\Gamma, x : A} & := & \monTy{\Gamma}, x : \monTy{A}\\
\monTyRel{\Gamma, x : A} & := & \monTyRel{\Gamma}
, x_0 : {\monTy{A}}_{0}
, x_1 : {\monTy{A}}_{1}
, x_\varepsilon : \monTyRel{A}\,x_0\,x_1
\end{array}
\]

\begin{center}
\textbf{Monotone translation on terms and types}
\end{center}
\vspace{0.5em}
\[
\begin{array}[t]{lcl}
\monTy{A} & := & \El\,\monTm{A} : \poset \\
\\
{\monTm{ x }} & := & x\\
{\monTm{\square{}_i}} & := & \uU_i \\[0.6em]
{\monTm{\P x : A . B}} & := & \PiU~\monTm{ A }~\monTmRel{\l x : A . B} \\
{\monTm{t~u}} & := & \monTm{t}~\monTm{u}\\
{\monTm{\l x : A . t}} & := & \l x : \monTy{ A } . \monTm{t} \\
{\monTm{\nat}} & := & \natU \\
{\monTm{\?_A}} & := & \?_{\monTm{A}}\\
{\monTm{\err_A}} &:= & \err_{\monTm{A}} \\
\monTm{\ascdom{t}{A}{B}} & :=&
\downcast{}_{\raisebox{-2pt}{\tiny$\ElRel{\monTm{B}{\sqsubseteq}\unkU}$}}\upcast_{\raisebox{-2pt}{\tiny$\ElRel{\monTm{A}{\sqsubseteq}\unkU}$}}\monTm{t}
\end{array}%
\begin{array}[t]{lcl}
\monTyRel{A} &:=& \ElRel\,\monTmRel{A} : \monTy{A} \distr \monTy{A}\\
\\
{\monTmRel{ x }} & := & x_\varepsilon\\
{\monTmRel{\square{}_i}} & := & \uU\dash{\sqsubseteq}_{i} \\[0.6em]
{\monTmRel{\P x : A . B}} & := & \PiU\dash{\sqsubseteq}~\monTmRel{ A
}~\monTmRel{\l x : A. B}\\
{\monTmRel{t~u}} & := & \monTmRel{t}~{\monTm{u}}_0~{\monTm{u}}_1~\monTmRel{u}\\
{\monTmRel{\l x : A .~t}} &:= &\l (x_0\,x_1 : \monTy{A})(x_\varepsilon :
\monTyRel{A}\,x_0\,x_1).~\monTmRel{t} \\
{\monTmRel{\nat}} & := & \natU\dash{\sqsubseteq} \\
{\monTmRel{\?_A}} & := & \texttt{refl}~\monTy{A}~\?_{\monTm{A}}\\
{\monTmRel{\err_A}} &:= & \texttt{refl}~\monTy{A}~\err_{\monTm{A}} \\
{\monTmRel{ \ascdom{t}{A}{B} }} &:= & \downcast{}_{\raisebox{-2pt}{\tiny$\ElRel{\monTm{B}{\sqsubseteq}\unkU}$}}\dash\texttt{mon}~\upcast_{\raisebox{-2pt}{\tiny$\ElRel{\monTm{A}{\sqsubseteq}\unkU}$}}\!\!\dash\texttt{mon}~\monTmRel{t}
\end{array}
\]
\vspace{0.5em}

${ \monTm{-} }_\alpha$ and ${ \monTy{-} }_\alpha$ where $\alpha \in \{0,1\}$
stand for the variable-renaming
counterparts of $\monTm{-}$ and $\monTy{-}$.
\caption{Translation of the monotone model}
\label{fig:monotone-translation}
\end{small}
\end{figure}

\subsection{Back to Graduality}
\label{sec:grad-term}
The precision order equipping each types of the monotone model can be reflected back to
\CCIC, giving rise to the {\em propositional precision} judgment:
\begin{align}
\label{def:propositional-precision}
\tcol{\Gamma} \caty \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u} \qquad := \qquad \exists e, \quad \monTyRel{\Gamma} \irty e : \monTm{t}
\precision{\monTm{T}}{\monTm{U}} \monTm{u}.
\end{align}
By the properties of the monotone model~(\cref{thm:universe-hierarchy}), there is at most one witness
up to propositional equality in the target that this judgment holds.
This precision relation bears a similar relationship to the structural precision
$$ as propositional equality with
definitional equality in \CIC{}.
On the one hand, propositional precision can be used to prove precision statements
inside the target type theory, for instance we can show by a straightforward
case analysis on $b : $ that $b :   b  A  A
□□ A$, a judgment that does not hold for syntactic precision.
In particular, propositional precision is compatible with propositional
equality, and a fortiori it is invariant by conversion in \CCIC: if
$t ≡t'$, $u ≡u'$ and
$Γ t TU u$
$Γ t' TU
On the other hand, propositional precision is not decidable, thus
not suited for typechecking, where structural precision has to be used instead.
\newcommand{\precBool}{\precision{\tcol{\bool}}{\tcol{\bool}}}

\begin{lemma}[Compatibility of structural and propositional precision]
\label{thm:prop-prop-prec}\text{}
\begin{enumerate}
\item If $\catyJ{}{t}{T}$, $\catyJ{}{u}{U}$ and $\vdash \tcol{t} \capre \tcol{u}$ then $\caty \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}$.
\item Conversely, if the target of the translation $\CICIRQ$ is logically
consistent and
$\caty \tcol{v_1} \precision{\tcol{\bool}}{\tcol{\bool}}
\tcol{v_2}$ for normal forms $\tcol{v_1}, \tcol{v_2}$, then
$\vdash \tcol{v_1} \capre \tcol{v_2}$.
\end{enumerate}
\end{lemma}
\begin{proof}
For the first statement, we strengthen the inductive hypothesis,
proving by induction on the derivation of structural precision the stronger
\begin{center}
If $\tcol{\GG} \vdash \tcol{t} \capre \tcol{u}$, $\tcol{\GG_1} \caty \tcol{t} : T$ and $\tcol{\GG_2} \caty \tcol{u} : \tcol{U}$
then there exists a term $e$ such that $\monTy{\GG} \irty e : \monTm{t} \precision{\monTm{T}}{\monTm{U}} \monTm{u}$.
\end{center}
The cases for variables (\nameref{infrule:capre-var}) and universes (\nameref{infrule:capre-univ}) hold by reflexivity.
The cases involving $\?$ (\nameref{infrule:capre-unk},
\nameref{infrule:capre-unk-univ}) and $\err$ (\nameref{infrule:capre-err}, \nameref{infrule:capre-err-lambda}) amount to $\monTm{\?}$ and
$\monTm{\err}$ being respectively interpreted as top and bottom elements at
each type.
For \nameref{infrule:capre-castr}, we have $\tcol{u} =
\tcol{\cast{A'}{B'}{t'}}$, $\tcol{B'} = \tcol{U}$, and
by induction hypothesis $\monTy{\GG} \vdash e : \monTm{t}
\precision{\monTm{{T}}}{\monTm{A'}} \monTm{t'}$
and $\monTy{\GG} \vdash \monTm{T} \sqsubseteq \monTm{B'}$.
Let $j$ be a universe level such that $\monTm{A'} \sqsubseteq \unkU[j]$,
$\monTm{B'} \sqsubseteq \unkU[j]$.
By (heterogeneous) transitivity of precision applied to $e$ and a witness of
$\monTy{\GG} \vdash \monTm{t'} \precision{\monTm{A'}}{\unkU[j]}
\upcast_{\monTm{A'} \sqsubseteq \unkU^j} \monTm{t'}$ (\cref{lem:adj}), we obtain a proof $e'$ of
$\monTy{\GG} \vdash e' : \monTm{t} \precision{\monTm{{T}}}{\monTm{B'}}
\upcast_{\monTm{A'} \sqsubseteq \unkU^j} \monTm{t'}$ and finally, using the
adjunction property,
a proof $e''$ of
\[\monTy{\GG} \vdash e : \monTm{t}
\precision{\monTm{{T}}}{\monTm{B'}}
\downcast_{\monTm{B'} \sqsubseteq \unkU^j}
\upcast_{\monTm{A'} \sqsubseteq \unkU^j} \monTm{t'} \equiv
\monTm{\cast{A'}{B'}{t'}} \equiv \monTm{u}.\]
The case \nameref{infrule:capre-castl} proceeds in an entirely symmetric fashion
since we only use the adjunction laws.
All the other cases, being congruence rules with respect to some term
constructor, are consequences of the monotonicity of said term constructor with a
direct application of the inductive hypothesis and inversion of the typing

For the second statement, by progress (\cref{thm:ccic-psafe}), both
$\tcol{v_1}$ and $\tcol{v_2}$ are canonical booleans, so we can proceed by case analysis on the canonical forms $\tcol{v_1}$ and $\tcol{v_2}$ that are either
$\tcol{\btrue}, \tcol{\bfalse}, \tcol{\err_\bool}$ or $\tcol{\?_\bool}$, ruling out the impossible cases by inversion of the
premise $\caty \tcol{v_1} \precBool \tcol{v_2}$ and logical consistency of $\irty$. Out of the $16$
cases, we obtain that only the following $9$ cases are possible:
\begin{array}{lrclrrclrrcl}
\caty & \tcol{\err_\bool} & \hspace{-1em} \precBool \hspace{-1em}  & \tcol{\err_\bool}
& \qquad \caty & \tcol{\err_\bool} &\hspace{-1em} \precBool \hspace{-1em} &  \tcol{\btrue}
& \qquad \caty & \tcol{\err_\bool} &\hspace{-1em} \precBool \hspace{-1em}  & \tcol{\bfalse} \\
\caty & \tcol{\err_\bool} & \hspace{-1em} \precBool \hspace{-1em}  & \tcol{\?_\bool}
& \caty & \tcol{\btrue} &\hspace{-1em} \precBool \hspace{-1em}  & \tcol{\btrue}
& \caty &  \tcol{\btrue} &\hspace{-1em} \precBool \hspace{-1em}  & \tcol{\?_\bool} \\
\caty & \hspace{-1em} \tcol{\bfalse} &\hspace{-1em} \precBool \hspace{-1em}  & \tcol{\bfalse}
& \caty & \hspace{-1em} \tcol{\bfalse} &\hspace{-1em} \precBool \hspace{-1em}   &\tcol{\?_\bool}
&\caty & \tcol{\?_\bool} &\hspace{-1em} \precBool \hspace{-1em}   & \tcol{\?_\bool}
\end{array}
For each case, a corresponding rule exists for the structural precision,
proving that $\vdash v_1 \capre v_2$.
\end{proof}

With a similar method, we show that
\CCICs satisfies graduality, which is the key missing point of
\cref{sec:gcic} and the \emph{raison d'etre} of the monotone model.

\begin{theorem}[Graduality for \CCICs]
\label{thm:graduality-gcics}
% \GCICP and
For $\tcol{\Gamma }\caty \tcol{t} : \tcol{T}, \tcol{\Gamma} \caty \tcol{t'} : \tcol{T}$ and $\tcol{\Gamma} \caty \tcol{u} : \tcol{U}$, we have

\begin{itemize}
\item (DGG) If
$\tcol{\Gamma} \caty \tcol{t} \precision{\tcol{T}}{\tcol{T}} \tcol{t'}$
then $ \tcol{t} \obsRef \tcol{t'}$;
\item (Ep-pairs)
If $\tcol{\Gamma} \caty \tcol{T} \precision{\tcol{\square}}{\tcol{\square}} \tcol{U}$ then
\[ \tcol{\Gamma} \caty \tcol{\cast{T}{U}{t}} \precision{\tcol{U}}{\tcol{U}} \tcol{u}
\Leftrightarrow  \tcol{\Gamma} \caty \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}
\Leftrightarrow  \tcol{\Gamma} \caty \tcol{t}
\precision{\tcol{T}}{\tcol{T}} \tcol{\cast{U}{T} u}, \]
Furthermore, $\tcol{\Gamma} \caty \tcol{{\cast{U}{T}{\cast{T}{U}{t}}} \equiprecise \tcol{t}}$.
\end{itemize}

\end{theorem}
\begin{proof}\mbox{}
\begin{itemize}
\item (DGG)
Let $\tcol{\mathcal{C}[ - ]} : (\tcol{\Gamma} \vdash \tcol{T}) \Rightarrow
(\vdash \tcol{\bool})$ be an observation context, by monotonicity of the
$\caty \tcol{\mathcal{C}[t]} \precBool \tcol{\mathcal{C}[t']}$.
By progress, subject reduction (\cref{thm:ccic-psafe}) and strong normalization
(\cref{thm:ccic-pnorm}) of $\CCICs$, there exists canonical forms
$\caty \tcol{v},\tcol{v'} : \tcol{\bool}$ such that $\tcol{\mathcal{C}[t]}
\conv \tcol{v}$ and $\tcol{\mathcal{C}[t']} \conv \tcol{v'}$.
Since propositional precision is stable by conversion in \CCIC, $\caty \tcol{v'}
\equiprecise \tcol{v}$.
Finally, we conclude that $\tcol{v} \conv \tcol{v'}$ by a case analysis on the boolean
normal forms $\tcol{v}$ and $\tcol{v'}$, that are either $\tcol{\btrue}, \tcol{\bfalse},
\tcol{\err_\bool}$ or $\tcol{\?_\bool}$: if $\tcol{v}$ and $\tcol{v'}$ are distinct normal
forms then $\caty \tcol{v'} \equiprecise \tcol{v}$ is a closed proof of an empty type,
contradicting the consistency of the target.
\item (Ep-pairs)
The fact that propositional precision induces an adjunction
is a direct reformulation of the fact that the relation
$\precision{\monTm{T}}{\monTm{U}}$ underlies an \eppair{}
(\cref{thm:universe-hierarchy}.(3)), using the fact that there is at most one
upcast and downcast between two types.
Similarly, the equi-precision statement is an application of the first point to the
\left\{
\begin{array}{l}
{\monTy{\Gamma} \irty \_ : \monTm{t} \precision{\monTm{T}}{\monTm{T}}
\monTm{\cast{T}{U}{\cast{U}{T}{t}}}} \\
{\monTy{\Gamma} \irty \_ : \monTm{\cast{U}{T}{\cast{T}{U}{t}}} \precision{\monTm{T}}{\monTm{T}}
\monTm{t}}
\end{array} \right .
which holds because $\downcast{}_{\monTm{T}\sqsubseteq\monTm{U}} \circ
\upcast{}_{\monTm{T}\sqsubseteq\monTm{U}} = \id{}$ in the monotone
\end{itemize}
\end{proof}

We conjecture that the target $$ mentioned in the above theorem and
propositions is consistent relative to a strong enough metatheory,\footnote{For
instance, $\mathcal{ZFC}$ + the existence of Mahlo cardinals~\cite{Setzer00,Forsberg13,DybjerS03}.} that is the
assumed inductive-recursive definition for the universe does not endanger
As can be seen from the proof, this hypothesis allows to move from a
contradiction internal to $$ to a contradiction in the ambient metatheory.

\subsection{Graduality of \CCICP}
\label{sec:grad-non-term}

To prove graduality of \CCICP, we need to provide a model accounting
for both monotony and non-termination.
The monotone model presented in the previous sections, which gives us
graduality for \CCICs and can be related to the pointed model of
\citet[Section 6.1]{NewLicatalmcs2020}, only accounts for terminating
In order to capture also non-termination, we can adapt the Scott model of
\citet[Section 6.2]{NewLicatalmcs2020} based on pointed $ω$-cpo to our
We now explain the construction of the main type formers, overloading the
notations from the previous sections.

Types are interpreted as bipointed $ω$-cpos, that is as orders $(A,
⊑)$ equipped with a smallest element $_A ∈A$, a largest element
$_A ∈A$ and an operation $sup_i a_i$ computing the suprema of countable ascending chains, \ie sequences $(a_i)_i∈ω ∈A^ω$ indexed by the ordinal $ω=
{0 < 1 < …}$ such that $a_i ⊑^A a_j$ whenever $i < j$.
A monotone function $f : A →B$ between $ω$-cpos is called
\emph{$\omega$-continuous} if for any ascending chain $(a_k)_k∈ω$, $sup_k f a_k
= f (sup_k a_k)$; we write $d : A  B$ for an \eppair{} between
$ω$-cpos where $_d$ preserves suprema (the left adjoint $_d$ automatically preserves suprema).

A type-theoretical construction of the free $ω$-cpo on a set is described
in~\cite{BidlingmaierFS19,ChapmanUV19} using quotient-inductive-inductive
types (QIIT)~\cite{AltenkirchCDKF18,KaposiKA19}.
We can adapt this technique to provide an interpretation for inductive types,
and in particular natural numbers, throwing in freely a new constructor $sup$
denoting the suprema of any chain of elements and quotienting by the appropriate
(in)equations: the suprema of a chain is greater than any of its parts $a_i
⊑sup a_i$ and an element $b$ that is greater than a chain $∀i, a_i ⊑b$ is greater than its suprema $supa_i ⊑b$.
Functions $f : A →B$ between types are interpreted as continuous monotone
maps, and the type $A B$ of continuous monotone
functions is an $ω$-cpo with suprema computed pointwise.
As in~\cref{sec:realizing-unknown-type}, the construction of the
$ω$-cpo corresponding to the unknown type is intertwined with the
universe hierarchy.
Assuming by induction that we have $ω$-cpos $_0$, \ldots, $_i$ for
universes at level lower than $i$, we follow the seminal work
of~\citet{scott76} on domains and we take the unknown type $[i+1]$ to be
a solution to the recursive equation:
\[\unkMon[i+1] \quad\cong\quad \liftNat + (\unkMon[i+1] \tocont \unkMon[i+1]) + \U_0 + \ldots + \U_i \]
The key techniques to build a solution to this equation in the setting of
$ω$-cpos are detailed in~\cite{SmythP77,Wand79}.
In a nutshell, this construction amounts to iterate the assignment $F(X) :=
+ (X X) + _0 + …+ _i$
starting from the initial bipointed $ω$-cpo
$$---the free bipointed $ω$-cpo on an empty
type, consisting just of $ ⊑$---and to take the colimit of the induced sequence:
\begin{align}
\label{eq:colimUnkMon}
\liftZero \distrcont F(\liftZero) \distrcont \ldots\> F^k(\liftZero)\> \ldots\>
\distrcont   \mathrm{colim}_k\,F^k(\liftZero) =: \unkMon[i+1]
\end{align}
For this construction to succeed, $F$ should extend to an $ω$-continuous
functor on the category of $ω$-cpos and $ω$-continuous \eppairs{} that
moreover preserves countable sequential colimits as above so that the following hold:
\[\unkMon[i+1] = \mathrm{colim}_k\,F^k(\liftZero) \cong
\mathrm{colim}_k\,F^{k+1}(\liftZero) \cong F(\mathrm{colim}_k\,F^k(\liftZero)) = F(\unkMon[i+1]).\]
The construction of $[i+1]$ as a fixpoint for $F$ should be contrasted
with the construction from~\cref{sec:realizing-unknown-type} where we
essentially describe explicitly a construction of $[i+1] :=
F([i])$ in the setting of bipointed posets.
The existence of countable sequential colimits in the category of $ω$-cpos
and \eppairs{}, as employed in \cref{eq:colimUnkMon}, is an interesting fact
proved in \cite[Theorem 3.1]{Wand79}, which we also use to equip the next universe
of codes $_i+1$ with an $ω$-cpo structure.
In brief, we adapt the inductive description of the universe of codes $_i$
given in~\cref{fig:IRUniverse} with an additional code $sup (A_k)_k ∈ω : _i$ for suprema of chains of codes $A_k : _i$, and
decode it with the function $$ satisfying $ (sup (A_k)_k ∈ω) ≅colim_k  ( A_k)$.
However, the isomorphism above cannot be used as a definition because
the definition of $$ has to respect the quotiented nature of
$_i$. In particular, when the chain is the constant chain $()_k ∈ω$, $sup ()_k ∈ω = $ and thus
$ (sup ()_k ∈ω)$
must also be equal to $$, which is different from $colim_k  $.
Technically, we define $ A$ as its isomorphic image onto $[i]$,
recovering a canonical choice for the inhabitants of $ (sup (A_k)_k ∈ω)$.

Note that in contrast with the construction from~\cref{sec:realizing-unknown-type}
that depended on $i$ and hence $_i$, the present construction of
$[i]$ does not depend on the construction of $_i$ and $_i$,
cutting the non-wellfounded loop observed in~\cref{sec:bare-model}.

The components that we describe assemble as a model of \CCICP into
\CICIRQ. In order to be able to prove DGG for \CCICP, we first need to
characterize the semantic interpretation of diverging terms of type $$ in the
\begin{lemma}
\label{lem:diverge-err}
If $\tcol{\Gamma} \caty \tcol{t} \inferty \tcol{\bool}$ and $\tcol{t}$ has no weak head
normal form, then $\monTm{\tcol{t}} = \err_{\monTm{{\tcol{\bool}}}}$.
\end{lemma}
\begin{proof}
The proof of this lemma is based on the definition of a logical
relation which is shown to relate $\tcol{t}$ to its translation
$\monTm{\tcol{t}}$ in the model (a.k.a. the fundamental lemma).
The precise definition of the logical and proof of the fundamental
lemma is given in~\cref{sec:divergence-omega-cpo-model}.
\end{proof}

Relativizing the notion of precision $Γ t
TS u$ of the monotone model to use the order
induced by this $ω$-cpo model instead of the monotone model,
we can replay the steps of
\cref{thm:graduality-gcics} and derive graduality for \CCICP.

\begin{theorem}[Graduality for \CCICP]
\label{thm:GCICP-graduality}
For $\tcol{\Gamma }\caty \tcol{t} : \tcol{T}, \tcol{\Gamma} \caty \tcol{t'} : \tcol{T}$ and $\tcol{\Gamma} \caty \tcol{u} : \tcol{U}$, we have

\begin{itemize}
\item (DGG) If $\tcol{\Gamma} \caty \tcol{t} \precision{\tcol{T}}{\tcol{T}} \tcol{t'}$
then $ \tcol{t} \obsRef \tcol{t'}$;
\item (Ep-pairs)
If $\tcol{\Gamma} \caty \tcol{T} \precision{\tcol{\square}}{\tcol{\square}} \tcol{U}$ then
\[ \tcol{\Gamma} \caty \tcol{\cast{T}{U}{t}} \precision{\tcol{U}}{\tcol{U}} \tcol{u}
\Leftrightarrow  \tcol{\Gamma} \caty \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}
\Leftrightarrow  \tcol{\Gamma} \caty \tcol{t}
\precision{\tcol{T}}{\tcol{T}} \tcol{\cast{U}{T} u}, \]
Furthermore, $\tcol{\Gamma} \caty \tcol{{\cast{U}{T}{\cast{T}{U}{t}}} \equiprecise \tcol{t}}$.
\end{itemize}

\end{theorem}

\begin{proof}\mbox{ }
\begin{itemize}
\item (DGG)
Similarly to the proof of \cref{thm:graduality-gcics}, we consider
a context $\tcol{\mathcal{C}[ - ]} : (\tcol{\Gamma} \vdash \tcol{T}) \Rightarrow
(\vdash \tcol{\bool})$. We know  by monotonicity of the
translation that $\caty \tcol{\mathcal{C}[t]} \precBool \tcol{\mathcal{C}[t']}$.
We need to distinguish whether the evaluation of $\tcol{\mathcal{C}[t]}$ and
$\tcol{\mathcal{C}[t']}$ terminates or not.
If $\tcol{\mathcal{C}[t]}$ diverges, we are done. If $\tcol{\mathcal{C}[t]}$
terminates and $\tcol{\mathcal{C}[t']}$ diverges, by progress,
$\tcol{\mathcal{C}[t]}$ reduces to a value $\tcol{v}$ and by
\cref{lem:diverge-err}, $\monTm{\tcol{\mathcal{C}[t']}} =
\err_{\monTm{{\tcol{\bool}}}}$.
This means that $\monTm{\tcol{\mathcal{C}[t]}} =
\err_{\monTm{{\tcol{\bool}}}}$ because $\err_{\monTm{{\tcol{\bool}}}}$ is
the smallest element of $\liftBool$.
Since $\monTm{-}$ is stable by conversion, $\monTm{\tcol{v}} =
\monTm{\tcol{\mathcal{C}[t]}} = \err_{\monTm{{\tcol{\bool}}}}$, and so
$\tcol{v} = \err_{\tcol{\bool}}$ by case analysis of the possible values for
If both terminates, then the reasoning is the same as in the proof of
\cref{thm:graduality-gcics}.

\item (Ep-pairs)
As for \cref{thm:graduality-gcics}, this fact derives directly from the
interpretation of the precision order as \eppairs in the $\omega$-cpo model.
\end{itemize}
\end{proof}

\section{Gradual Indexed Inductive Types}
\label{sec:giit}

We now explore how indexed inductive types, as used in the introduction (\cref{ex:indices}), can be handled in \GCIC.
Recall the definition of \coqe{vec}:
\begin{coq}
Inductive vec (A : Type) : nat -> Type :=
| nil  : vec A 0
| cons : A -> forall n : nat, vec A n -> vec A (S n).
\end{coq}
and recall the difference between {\em parameters} (here, \coqe{A}), which are common to all constructors, and {\em indices} (here, \coqe{n}), which can differ between constructors.
Also recall from \cref{sec:bidirectional-cic} that our formal development does not consider indexed inductive types, only parametrized ones.

This section first explains two alternatives to indexed inductive types that can directly be expressed in \GCIC (\cref{sec:alt-indices}). We then describe how these alternatives actually behave in the gradual setting (\cref{sec:index-induct-type,sec:decid-equal-more}). Finally, we present an extension of \CCIC to directly support indexed inductive types, focusing on the specific case of vectors (\cref{sec:case-vectors}), showing that it combines the advantages of the other approaches. \cref{sec:giit-summary} summarizes our findings.

\subsection{Alternatives to indexed inductive types}
\label{sec:alt-indices}

Indexed inductive types make it possible to define structures that are intrinsically characterized by some property, which holds by construction, as opposed to extrinsically establishing such properties after the fact. There are two well-known alternatives to indexed inductive types for capturing properties intrinsically: type-level fixpoints, and ``forded'' inductive types.

\begin{description}
\item[Type-level fixpoint.] The vector can be defined as a recursive function on the index, at the type level. For instance, the following formulation represents sized lists as nested pairs:

\begin{coq}
Fixpoint FVec (A : Type) (n : nat) :Type := match n with 0 => unit | S n => A * FVec A n end.
\end{coq}
Type-level fixpoints can be used as soon as the indices are \emph{concretely
forceable}~\cite{bradyEtAl:types2004}. Intuitively, concretely forceable indices are those that can be matched upon (like \coqe{n} in this example definition). See \citet{GilbertCST19} for a description of a general translation.

\item[Forded inductive type.] Instead of using an indexed inductive type, one can use a parametrized inductive type, with {\em explicit} equalities as arguments to constructors.%
\footnote{This technique has reportedly been coined ``fording'' by \citet[\textsection 3.5]{mcbride99}. Fording is in allusion to the Henry Ford quote {\em ``Any customer can have a car painted any color that he wants, so long as it is black.''}}
For instance, vectors can be defined in this style as follows:
\begin{coq}
Inductive vec_eqdec (A : Type) (n : nat) : Type :=
| nil_eqdec : eq_nat 0 n -> vec_eqdec A n
| cons_eqdec : A -> forall m : nat, eq_nat (S m) n -> vec_eqdec A m -> vec_eqdec A n.
\end{coq}
Note that this definition uses \coqe{eq_nat}, the type of decidable equality proofs over natural numbers, for expressing the constraints on \coqe{n} instead of propositional equalities (\eg~\coqe{0=n}), because propositional equality is not available in \GCIC (\cref{sec:limit-propeq}).
\end{description}

In \CIC, these two alternative presentations of an indexed inductive type can be shown internally to be
equivalent. But each of these presentations has advantages and drawbacks depending on the considered system and scenarios of use, so practitioners have different preferences in that respect. More important to us here, these presentations are {\em not} equivalent in \GCIC.

\subsection{Type-level fixpoints}
\label{sec:index-induct-type}

\paragraph{Constructors.}
The definition of \coqe{FVec} above can directly be written in \GCIC, as it
uses only inductive types with parameters (here the unit and product
types and natural numbers).
The vector constructors can be defined as:
\begin{coq}
Definition Fnil (A:Type) : FVec A 0 := tt.
\end{coq}
\begin{coq}
Definition Fcons (A:Type) (a:A) (n:nat) (v:FVec A n) : FVec A (S n) := (a , v).
\end{coq}
whose definitions typecheck because \coqe{FVec} computes on its

\paragraph{Behavior.}
Let us now look at the type computed at $_$. Because $_$ is an
exceptional term, the fixpoint has to return unknown in the universe:
\coqe{FVec A ?_nat ==* ?_Type}. This means that the mechanism for
casting a vector into a vector with the unknown index is directly
inherited from the generic mechanism for casting to the unknown type.
Therefore, we get for free the following computation rules, because
they involve embedding-projection pairs:
\begin{coq}
Fnil A::FVec A ?_nat::FVec A 0 ==* Fnil A
\end{coq}
\begin{coq}
Fnil A::FVec A ?_nat::FVec A 1 ==* raise
\end{coq}

Similarly, the eliminator \coqe{FVec_rect} can be defined by first
matching on the index, and then on the vector and satisfies the
computation rule of vectors when the index is non-exceptional.
The only drawback of this encoding is that the behavior of the
eliminator is not satisfactory when the index is unknown.
Consider for instance the following term from \cref{ex:indices}, which unfortunately reduces to
\coqe{?_nat}:
\begin{coq}
Fhead ?_nat (Ffilter nat 4 even [ 0 ; 1 ; 2 ; 3 ]) ==* ?_nat
\end{coq}
\noindent
This behavior occurs because the eliminator starts by
matching on the index, which is unknown, and thus has to return the
unknown itself.

\subsection{Fording with decidable equalities}
\label{sec:decid-equal-more}

\paragraph{Constructors}

With the definition of the forded inductive type \coqe{vec_eqdec},
the \coqe{nil_eqdec} constructor can legitimately be used to inhabit
\coqe{vec_eqdec A ?_nat}, provided we have an inhabitant (possibly \?)
of \coqe{eq_nat 0 n}.

Note that we can provide the same vector interface as that of the indexed inductive type by
defining the following constructor wrappers,
using the term \coqe{refl n} of reflexivity on \coqe{eq_nat}:
\begin{coq}
Definition nil' (A:Type) : vec_eqdec A 0 := nil_eqdec A (refl 0).
\end{coq}
\begin{coq}
Definition cons' A a n (v: vec_eqdec A n) : vec_eqdec A (S n) := cons_eqdec A a n (refl n) v.
\end{coq}
and define the corresponding eliminator \coqe{vec_rect'} accordingly.

\paragraph{Behavior.}

The computational content of the eliminator on
\coqe{vec_eqdec A ?_nat} is more precise than with \coqe{FVec}: the
eliminator never matches on the proof of equality to produce a term,
but only to guarantee that a branch is not accessible.
Concretely, this means that we observe the expected reduction:
\begin{coq}
nil_eqdec A e::vec_eqdec A ?_nat::vec_eqdec A 0 ==* nil_eqdec A e
\end{coq}
Again, the fact that upcasting to \coqe{vec_eqdec A ?_nat} and then
downcasting back is the identity relies on the \CCIC mechanism on the unknown
for the universe, but this time only for the type representing the
decidable equality.
Likewise, the example of \coqe{filter} (\cref{ex:indices}) computes as expected:
\begin{coq}
Dhead ?_nat (Dfilter nat 4 even [ 0 ; 1 ; 2 ; 3 ]) ==* 0
\end{coq}

On the other hand, an invalid assertion does not produce an error, but a term with an error in place of the equality proof:
\begin{coq}
nil_eqdec A e::vec_eqdec A ?_nat::vec_eqdec A 1 ==* nil_eqdec A raise
\end{coq}
where \coqe{raise} is at type \coqe{eq_nat 1 0}.
Consequently, we have \coqe{Dhead ?_nat (Dfilter nat 2 even [ 1 ; 3 ]) ==* raise},
because the branch of \coqe{Dhead} that deals with the \coqe{nil} case matches
on the (erroneous) equality proof.
Invalid assertions are therefore very lazily observed, if at all, which is not satisfactory.

Finally, there is a drawback of using decidable equalities, which only manifests when working with the original vector interface (\coqe{nil'}/\coqe{cons'}/\coqe{vec_rect'}).
In that case, the eliminator does not enjoy the expected computational rule
on the constructor \coqe{cons'}.
Because the eliminator is defined by induction on natural numbers, therefore it only reduces
when the index is a concrete natural number, not a variable.

\subsection{Direct support for indexed inductive types: the case of vectors}
\label{sec:case-vectors}

\begin{figure}
\small
\begin{mathpar}
\inferrule{  }{\can{\GnilU{A}}}
\and
\inferrule{ }{\can{(\GconsU{A}{a}{n}{v})}}
\\
\redrule{
\ascdom{(\Gcons{A}{a}{k}{v})}{\Gvect{A}{(S~n)}}{\Gvect{B}{\?_\nat}}
\GconsU{B}{(\ascdom{a}{A}{B})}{n}{(\ascdom{v}{\Gvect{A}{k}}{\Gvect{B}{n}})}
\hfill

\\
\redrule{
\ascdom{(\Gcons{A}{a}{k}{v})}{\Gvect{A}{(S~n)}}{\Gvect{B}{(S~m)}}
\hfill}[V-cons]\label{red:v-S}
\\
\redrule{
\ascdom{(\Gcons{A}{a}{k}{v})}{\Gvect{A}{(S~n)}}{\Gvect{B}{0}}
\err_{\Gvect{B}{0}} \myflushright
\\

\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{\GnilU{A}}
{\ascdom{(\GvectRec{P}{P_{nil}}{P_{cons}}{\Gnil{A}})}{P~0}{P~\?_\nat} \hfill
\\
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{(\GconsU{A}{a}{n}{v})}
\\
\myflushright \ascdom{(\GvectRec{P}{P_{nil}}{P_{cons}}{(\Gcons{A}{a}{n}{v})})}{P~(S~n)}{P~\?_\nat}

\end{mathpar}
\caption{New canonical forms and reduction rules for vectors in \CCIC (excerpt).}
\label{fig:vectors-excerpt}
\end{figure}

Extending \GCIC/\CCIC with direct support for indexed inductive types can provide a fully satisfactory solution, in contrast to the two previously-exposed encodings that both have serious shortcomings.
The idea is to reason about indices directly in the reduction of casts.
Here, we expose this approach for the specific case of length-indexed vectors and leave a generalization to future work.
\cref{sec:case-vectors-appendix} describes the extension for vectors in full details; here,
we only present selected rules (\cref{fig:vectors-excerpt}) and illustrate how reduction works.

\paragraph{Constructors}
We add two new canonical forms,
corresponding to the casts of \coqe{nil} and \coqe{cons} to
$A_$: namely, $A$ and
$Aanv$ (\cref{fig:vectors-excerpt}).
Note that we cannot simply declare casts such as
$tAnA_$ to be canonical,
because they involve non-linear occurrences of types (here, $A$).

\paragraph{Reduction rules}
We add reduction rules to conduct casts between vectors
in canonical forms. \cref{fig:vectors-excerpt} presents these rules
when the argument of the cast is a \coqe{cons}.
Rule~\nameref{red:v-S?} propagates the cast on the arguments,
but using the newly-introduced $$, effectively converting precise
information to less precise information.
Rule~\nameref{red:v-S} applies when both source and target indices are successors,
and propagates the cast of the arguments, just like the
standard rule for casting a constructor.
As expected, Rule~\nameref{red:v-S0} raises an error when the indices do not match.

For the eliminator, there are two new computation rules, one for each
new constructor: \nameref{red:v-rect-unk-0} and
\nameref{red:v-rect-unk-S}. They both apply the eliminator to the
underlying non-exceptional constructor, and then cast the result back
to $P _$.
Intuitively, these rules transfer the cast on vectors to a cast on
the returned type of the predicate.

\paragraph{Behavior}
Given these rules, we can actually realize the behavior described in
\cref{ex:indices}. For instance, we have both
\begin{coq}
nil A::vec A ?_nat::vec A 0 ==* nil A
\end{coq}
\begin{coq}
nil A::vec A ?_nat::vec A 1 ==* raise_A
\end{coq}
and coming back to \cref{ex:indices}, in all three \GCIC variants the term:

\begin{center}
\coqe{head ?_nat (filter nat 4 even [ 0 ; 1 ; 2 ; 3 ])}
\end{center}
\noindent typechecks and reduces to \coqe{0}. Additionally, as expected:

\begin{center}
\coqe{head ?_nat (filter nat 2 even [1 ; 3])}
\end{center}
\noindent typechecks and fails at runtime. And similarly for \cref{ex:specif}.

Note that to be able to define the action of casts on vectors, we have
crucially used the fact that it is possible to discriminate between
\coqe{0}, \coqe{S n} and $_$ in the reduction rule.

\subsection{Summary}
\label{sec:giit-summary}
To summarize, the different approaches to define structures with intrinsic properties in \GCIC compare as follows:
\begin{itemize}
\item The type-level fixpoint coincides with the indexed inductive presentation
on non-exceptional terms, but is extremely imprecise in presence of unknown indices.
\item The forded inductive is more accurate when dealing with unknown indices, but is arguably too permissive with invalid index assertions.
\item The direct support of the indexed inductive type with additional constructors and reduction rules yields a satisfactory solution. We conjecture that this presentation can be generalized to support arbitrary indexed inductive types as long as they have
concretely forceable indices; we leave such a general construction for future work.
\end{itemize}
Recall that fording is only an option in \GCIC when the indices pertain to a type with decidable equality; properly handling general propositional equality in a gradual type theory
is an open question (\cref{sec:limit-propeq}).
The constraint of indices being concretely forceable (for type-level fixpoints, direct support)
are intuitively understandable and expected: gradual typing requires synthesizing dynamic checks, therefore these checks need to be somehow computable.

\section{Limitations and Perspectives}
\label{sec:future-cic}

Up to now, we have left aside three important aspects of \CIC, namely,
impredicativity, $η$-equality and propositional equality.
This section explains the challenges induced by each feature, and possibly,
venues to explore.

\subsection{Impredicativity}

In this work, we do not deal with the impredicative sort
\texttt{Prop}, for multiple reasons.
The models used in \cref{sec:realizing-ccic} to justify termination and
graduality crucially rely on the predicativity of the universe hierarchy for the
inductive-recursive definition of codes to be well-founded.
Moreover, the results of \citet[Theorem 6.1]{Palmgren98} show that it is not
possible to endow an impredicative universe with an inductive-recursive
structure in a consistent and strongly-normalizing theory,
hinting that it may be difficult to devise an inductively-defined cast
function between types that belong to an impredicative universe.
Additionally, it seems difficult to avoid the
divergence of $Ω$ with an impredicative sort, as no universe levels can
be used to prevent a self-application from
being well-typed.

\subsection{$\eta$-equality}

In most presentations of \CIC, and in particular its \Coq
implementation, conversion satisfies an additional rule, called
$η$-equality, which corresponds to an extensional property for
\Gamma \vdash f \conv \l x : A . f~x \quad \mbox{when} \quad \Gamma \vdash f:\Pi x:A . B.
The difficulty of integrating $η$-equality in the setting of \GCIC is that the conversion we consider in \CCIC is entirely induced
by a notion of reduction: two
terms are convertible exactly when they have a common reduct up to
It is well-known that $η$-equality cannot be easily modeled using a
rewrite rule, as both $η$-expansion and $η$-reduction have significant
drawbacks~\cite{10.1145/1047659.1040312}, and so we would have to consider another
approach to the one we took if we were to integrate $η$-equality.
The most prominent alternative way is to define conversion
as an alternation of reduction steps (for instance using a weak-head
reduction strategy) not containing $η$ and comparison of terms up to congruence and $η$-equality.

This approach has been recently formalized by \citet{Abel:POPL2018} in a fully-typed setting. That is, types participate crucially
in the conversion relation: they are maintained during conversion, so that for instance comparison of terms at a $Π$-type systematically $η$-expands them
before recursively calling conversion at the domain types.
Defining a gradual variant of such a typed conversion might be quite interesting,
but would require a significant amount of work.

On the contrary, a precise, formalized, account is still missing for $η$-equality for an untyped conversion as used in practice in the \Coq proof assistant and in \GCIC.
The MetaCoq project, which aims at such a formalized account, leaves the treatment of $η$-equality to future work~\cite{SozeauBFTW20}.
While we envision no specific issues to the adaptation to this approach
to gradual typing once a clear and precise solution for
\CIC itself has been reached, solving the issue in a satisfactory way for
\CIC is obviously out of scope for this article.
Thus, while it should in principle be possible to add $η$-equality to \GCIC,
either via typed or untyped conversion,
we leave this for future work.

\subsection{Propositional equality}
\label{sec:limit-propeq}

In \CIC, propositional equality \coqe{eq A x y}, corresponds to the Martin-L{\"o}f
identity type~\cite{Martin-Lof-1973}, with a single constructor \coqe{refl} for reflexivity, and the
elimination principle known as \coqe{J}:
\begin{coq}
Inductive eq (A : Type) (x : A) : A -> Type := refl : eq A x x.
\end{coq}
\begin{coq}
J : forall (A : Type) (P : A -> Type) (x : A) (t : P x) (y : A) (e : eq A x y), P y
\end{coq}
together with the conversion rule:

\begin{center}
\coqe{J A P x t x (refl A x) equiv t}
\end{center}

For the sake of exposing the problem, suppose that we can define this identity type in \GCIC,
while still satisfying canonicity, conservativity with respect to \CIC and graduality.
This means that for an equality \coqe{t = u} involving closed terms
\coqe{t} and \coqe{u} of \CIC, there
should only be three possible canonical forms: \coqe{refl A t} whenever \coqe{t} and \coqe{u} are convertible terms (of type \coqe{A}), as well as \coqe{raise} and \coqe{?}.

Just under these assumptions,
we can show that there exist two functions that are pointwise equal in \CIC, and hence equal by extensionality, but are no longer equivalent in \GCIC/\CCIC.
Consider the two functions \coqe{id_nat} and \coqe{add0} below:
\begin{coq}
id_nat := fun n : nat => n         add0 := fun n : nat => n + 0
\end{coq}
In \CIC, these functions are not convertible, but they are observationally equivalent.
However, they would not be observationally equivalent in \GCIC.
To see why, consider the following term:

\begin{coq}
test := fun f => J (nat -> nat) (fun _ => bool) id_nat true f (refl id_nat::?_Type::id_nat = f)
\end{coq}
We have \coqe{test id_nat ==* true} because, by \pgrad,
\coqe{refl id_nat::?_Type::id_nat = id_nat ==* refl id_nat}.
However, because \coqe{add0} is {\em not} convertible to \coqe{id_nat},
\coqe{refl id_nat::id_nat = add0} cannot possibly reduce to \coqe{refl}, and
thus would need to reduce either to $$ or \?; and so does \coqe{test add0}.

This means that a model for such a gradual type theory would need to be intensional, conversely to the extensional models usually used to justify type theories. Studying such a model as well as exploring alternatives approaches to propositional equality in a gradual type theory are interesting venues for future work.

\section{Related Work}
\label{sec:related}

\mparagraph{Bidirectional typing and unification}
Our framework uses a bidirectional version of the type system of
\CIC.
Although this presentation is folklore among type theory
specialists~\cite{McBride2019}, the type system of \CIC is rarely
presented in this way on paper and has been studied in details only
However, the bidirectional approach becomes necessary when dealing
with unification and elaboration of implicit arguments.
Bidirectional elaboration is a common feature of proof assistant
implementations, for instance \cite{Asperti2012}, as it clearly delineates what
information is available to the elaboration system in the different typing
modes. In a context with missing information due to implicit arguments, those
implementations face the undecidable higher order unification \cite{Dowek2001}.
In this error-less context, the solution must be a form of under-approximation,
using complex heuristics \cite{Ziliani2017}. Deciding consistency is very close
to unification, as observed by \citet{castagnaAl:popl2019}, but our notion of
consistency over-approximates unification, making sure that unifiable terms are
always consistent, relying on errors to catch invalid over-approximations at

\mparagraph{Dependent types with effects}
As explained in this paper, introducing the unknown type of gradual
typing also require, in a dependently-typed setting, to introduce
unknown terms at any type. This means that a gradual dependent type
theory naturally endorses an effectful mechanism which is similar to
having exceptions.
This connects \GCIC to the literature on dependent types and effects.
Several programming languages mix dependent types with effectful computation, either giving up on metatheoretical properties, such as Dependent Haskell~\cite{eisenberg2016dependent}, or by restricting the dependent fragment to pure expressions~\cite{xiPfenning:pldi98,swamyAl:popl2016}.
In the context of dependent type theories,
\citet{PedrotT17,pedrotTabareau:esop2018} have leveraged the monadic approach to
type theory, at the price of a weaker form of dependent large
elimination for inductive types.
The only way to recover full elimination is to accept a weaker form of
logical consistency, as crystallized by the fire triangle between
observable effects, substitution and logical

\mparagraph{Ordered and directed type theories}
The monotone model of \CCIC interpret types as posets in order to
give meaning to the notion of precision.
Interpretations of dependent type theories in ordered structures goes back to
various works on domain theoretic and realizability interpretations of (partial)
Martin-Löf Type Theory~\cite{PalmgrenS90,Ehrhard88}.
More recently, \citet{LicataH11} and \citet{North19} extend type theory with directed
structures corresponding to a categorical interpretation of types, a higher
version of the monotone model we consider.

\mparagraph{Hybrid typing} \cite{ouAl:tcs2004} present a programming language with separate dependently- and simply-typed fragments, using arbitrary runtime checks at the boundary. \citet{knowlesFlanagan:toplas2010} support runtime checking of refinements. In a similar manner, \cite{tanterTabareau:dls2015} introduce casts for subset types with decidable properties in \Coq. They use an axiom to denote failure, which breaks weak canonicity. Dependent interoperability \cite{oseraAl:plpv2012,dagandAl:jfp2018} supports the combination of dependent and non-dependent typing through deep conversions.
All these approaches are more intended as programming languages than as type theories, and none support the notion of (im)precision that is at the heart of gradual typing.

\mparagraph{Dependent contracts}
\cite{greenbergAl:popl2010} relates hybrid typing to dependent contracts, which are dynamically-checked assertions that can relate the result of a function application to its argument~\cite{findlerFelleisen:icfp2002}. The semantics of dependent contracts are subtle because contracts include arbitrary code, and in particular one must be careful not to violate the precondition on the argument in the definition of the postcondition contract~\cite{bloomMcAllester:jfp2006}.  Also, blame assignment when the result and/or argument are themselves higher-order is subtle. Different variants of dependent contracts have been studied in the literature, which differ in terms of the violations they report and the way they assign blame~\cite{greenbergAl:popl2010,dimoulasAl:popl2011}.
An in-depth exploration of blame assignment for gradual dependent type theories such as \GCIC is an important perspective for future work.

\mparagraph{Gradual typing}
The blame calculus of \citet{wadlerFindler:esop2009} considers subset types on base types, where the refinement is an arbitrary term, as in hybrid type checking \cite{knowlesFlanagan:toplas2010}. It however lacks the dependent function types found in other works.
\citet{lehmannTanter:popl2017} exploit the Abstracting Gradual Typing (AGT) methodology~\cite{garciaAl:popl2016} to design a language with imprecise formulas and implication. They support dependent function types, but gradual refinements are only on base types refined with decidable logical predicates.
\citet{eremondiAl:icfp2019} also use AGT to develop approximate normalization and GDTL. While being a clear initial inspiration for this work, the technique of approximate normalization cannot yield a computationally-relevant gradual type theory (nor was its intent, as clearly stated by the authors). We hope that the results in our work can prove useful in the design and formalization of such gradual dependently-typed programming languages. \citet{eremondiAl:icfp2019} study the dynamic gradual guarantee, but not its reformulation as graduality~\cite{newAhmed:icfp2018}, which as we explain is strictly stronger in the full dependent setting. Finally, while AGT provided valuable intuitions for this work,
graduality as embedding-projection pairs was the key technical driver in the design of \CCIC.

\section{Conclusion}
\label{sec:conclusion}

We have unveiled a fundamental tension in the design of gradual dependent type
theories between conservativity with respect to a dependent type theory such as \CIC,
normalization, and graduality.
We explore several resolutions of this Fire Triangle of Graduality, yielding
three different gradual counterparts of \CIC, each compromising with one
edge of the Triangle.
We develop the metatheory of all three variants of \GCIC thanks to a common
formalization, parametrized by two knobs controlling universe constraints on
dependent product types in typing and reduction.

This work opens a number of perspectives for future work, in addition to addressing the limitations discussed in \cref{sec:future-cic}.
The delicate interplay between universe levels and computational
behavior of casts begs for a more flexible approach to the
normalizing \GCICT, for instance using gradual universes.
The approach based on multiple universe hierarchies to support logically
consistent reasoning about exceptional programs~\cite{pedrotAl:icfp2019} could
be adapted to our setting in order to provide a seamless integration
inside a single theory of gradual features together with
standard \CIC without compromising normalization.
This could also open the door to supporting consistent reasoning about gradual
programs in the context of \GCIC.
On the more practical side, there is still a lot of challenges ahead in order to implement a gradual incarnation of \GCIC in \Coq or \Agda, possibly parametrized in order to support the three variants presented in this work.

\bibliography{strings,pleiad,bib,common,refs}

\ifappendix
\clearpage
\appendix

\section{Index of notations}
\label{sec:notations}
\begin{center}
\begin{tabular}{|c|c|c|p{0.35\textwidth}|}
\hline
Description & Symbol & Ref & Remark\\
\hline
\multicolumn{4}{|c|}{Section \labelcref{sec:bidirectional-cic}} \\
\hline
Universe & $[]_i$ & \cpageref{fig:syntax-cic} & At level $i$\\
Inductive type & $I\ulev{i}(\orr{a})$ & \cpageref{fig:syntax-cic} & At level $i$ with parameters $\orr{a}$ \\
Inductive constructor & $ c_k^I\ulev{i}(\orr{a},\orr{b})$ & \cpageref{fig:syntax-cic} & $k$-th constructor of $I$ at level $i$ with parameters $\orr{a}$ and arguments $\orr{b}$ \\
Inductive destructor & $\match{I}{s}{z.P}{f.\orr{y}.\orr{b}}$ & \cpageref{fig:syntax-cic} & corresponds to fix + match in Coq \\
Substitution & $t\subs{u}{x}$ & \cpageref{fig:syntax-cic} & extended to parallel substitution \\
Types of parameters & $\pars(I,i)$ & \cpageref{params} & of inductive $I$ at level $i$ \\
Types of arguments & $\args(I,i,c_k)$ & \cpageref{params} & of constructor $k$ of inductive $I$ at level $i$ \\
Substitution in parameters & $\pars(I,i)\parsub{\orr{a}}$ & \cpageref{params} & \\
Substitution in arguments & $\args(I,i,c_k)\parsub{\orr{a}, \orr{b}}$ & \cpageref{params} & \\
Context checking & $\vdash \Gamma$ & \cref{fig:bidir} & \\
Type inference & $\Gamma \vdash t \inferty T$ & \cref{fig:bidir} & \\
Type checking & $\Gamma \vdash t \checkty T$ & \cref{fig:bidir} & \\
Constrained inference & $\Gamma \vdash t \pcheckty{\bullet}$ & \cref{fig:bidir} &
$\bullet$ is either $\Pi$, $I$ or $[]$ \\
One-step reduction & $\redCCIC$ & \cref{fig:bidir} & \emph{full}, \ie with all congruences \\
Reduction & $\rtred$ & \cref{fig:bidir} & reflexive, transitive closure of $\redCCIC$ \\
Conversion & $\conv$ & \cref{fig:bidir} & \\
\hline
\multicolumn{4}{|c|}{Section \labelcref{sec:gcic}} \\
\hline
Unknown type & $\tcol{\?_{T}}$ & \cpageref{fig:syntax-castcic} & in \CCIC \\
Error & $\tcol{\err_{T}}$ & \cpageref{fig:syntax-castcic} & \\
Cast & $\cast{\tcol{T}}{\tcol{T'}}{\tcol{t}}$ & \cpageref{fig:syntax-castcic} & \\
Level of product type & $\sortOfPi{i}{j}$ & \cref{fig:univ-param} & \\
Level of product germ & $\castOfPi{i}$ & \cref{fig:univ-param} & \\
Type heads & $\H$ & \cref{fig:head-germ} & \\
Head of a type & $\hd(\tcol{T})$ & \cref{fig:head-germ} & \\
Germ & $\stalkCIC{i}{h}$ & \cref{fig:head-germ} & Least precise type with head $h$ at level $i$ \\
Parallel reduction & $\paraRed$ & \cref{lem:confluence} & \\
Canonical term & $\can{\tcol{t}}$ & \cref{fig:CCIC-canonical} & inductive caracterization \\
Neutral term & $\neu{\tcol{t}}$ & \cref{fig:CCIC-canonical} & inductive caracterization \\
$\alpha$-consistency & $\tcol{t} \acons \tcol{t'}$ & \cref{fig:acons} & \\
Consistent conversion & $\tcol{t} \cons \tcol{t'}$ & \cref{def:cons} & Also called \emph{consistency} \\
Unknown type & $\scol{\?\ulev{i}}$ & \cpageref{gcic-syntax} & in \GCIC, at level $i$ \\
Elaboration (inference) & $\inferelab{}{t}{}{\Gamma}{t'}{T}$ & \cref{fig:elaboration} & \\
Elaboration (checking) & $\checkelab{}{t}{}{\Gamma}{t'}{T}$ & \cref{fig:elaboration} & \\
Elaboration (constrained) & $\pcheckelab{\bullet}{}{t}{}{\Gamma}{t'}{T}$ & \cref{fig:elaboration} & \\
Structural precision & $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$ & \cref{fig:apre-ccic} & extended to contexts pointwise \\
Definitional precision & $\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}$ & \cref{fig:apre-ccic} & extended to contexts pointwise \\
Typing in \CIC/\CCIC & $\cicty$ / $\caty$ & \cref{sec:gcic-theorems2} & to differentiate between systems \\
Equiprecision & $\tcol{\GG} \vdash \tcol{t} \caequipre \tcol{t'}$ & \cref{def:equipre} & \\
Erasure & $\eras(\tcol{t})$ & \cref{def:erasure} & \\
Syntactic precision & $\scol{t} \apre \scol{t'}$ & \cref{fig:apre-gcic} & \\
\hline

\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{|c|c|c|p{0.35\textwidth}|}
\hline
Description & Symbol & Ref & Remark\\
\hline
\multicolumn{4}{|c|}{Section \labelcref{sec:realizing-ccic}} \\
\hline
\CIC + Induction-Recursion & \CICIR &  \cref{sec:bare-model} & Target for the discrete model \\
Judgements for \CICIR & $\irty$ & & \\
\CICIR + quotients & \CICIRQ & & Target for the monotone models \\
Universe of codes &$\U$ & \cref{fig:discrete-univ} & \\
Bipointed poset on inductive I &$\liftErr{I}$ &  \cref{sec:bare-model} & \\
Top element in $\liftErr{I}$ & $\lifttop{\liftErr{I}}$ & \cref{sec:bare-model}& \\
Bottom element in $\liftErr{I}$ & $\liftbot{\liftErr{I}}$& \cref{sec:bare-model}& \\
Bipointed poset on % natural numbers
$\nat$ & $\liftNat{}$ & \cref{sec:bare-model}& \\
Bipointed poset on % dependent sum
$\Sigma$ & $\liftSigma{}$ & \cref{sec:bare-model}& \\
% Code for a type & $\code{.}$& & \\
Code for nat &$\natU$ & \cref{sec:bare-model}& \\
Code for dependent product& $\PiU$ & \cref{sec:bare-model}& \\
Code for universes &$\uU_i$ & \cref{sec:bare-model}& \\
Code for unknown types &$\unkU[i]$ & \cref{sec:bare-model}& \\
Code for error type &$\errU$ & \cref{sec:bare-model}& \\
Decoding function to types &$\El$ & \cref{fig:discrete-univ,fig:IRUniverse}& $\El : \U \to \poset$ \\
Type heads & $\H_i$ & \cref{fig:head-germ} & \\
Head of a type & $\hd(T)$ & \cref{fig:head-germ} & \\
Germ as a code &$\stalkCode{i}{h}$ & \cref{sec:bare-model} & \\
Germ & $\stalkCIC{i}{h}$ & \cref{fig:head-germ} & Least precise type with head ${h \in \H_i}$ at level $i$ \\
Cast in discrete model&$\cas$ & \cref{fig:cast-implem-discrete}&\\
Discrete translation of types &$\bareTy{\cdot}$ & \cref{fig:discrete-translation} & \\
Discrete translation of terms & $\bareTm{\cdot}$& \cref{fig:discrete-translation} & \\
Order on type $A$ & $\sqsubseteq^{A}$& \cref{sec:poset-model-dtt} &\\
Type of posets & \poset  & \cref{sec:poset-model-dtt} & \\
Monotone dependent product & $ \Pmon{}\,A\,B$  & \cref{sec:poset-model-dtt}& \\
Ep-pairs & $A \distr{} B$ & \cref{def:ep-pair} & \\
Upcast & $\upcast_d$ & \cref{def:ep-pair}& Embedding part of an \eppair{} $d$ \\
Downcast & $\downcast_d$ & \cref{def:ep-pair}& Projection part of an \eppair{} $d$ \\
Monotone unknown type & $\unkMon[i]$ & \cref{sec:realizing-unknown-type} & \\
Quotiented pairs in $\unkMon[i]$ & $\unkInj{h}{x}$ & \cref{sec:realizing-unknown-type}& \\
Top element in $\unkMon[i]$ & $\lifttop{\unkMon[i]}$ & \cref{sec:realizing-unknown-type}& \\
Bottom element in $\unkMon[i]$ & $\liftbot{\unkMon[i]}$& \cref{sec:realizing-unknown-type}& \\
Decoding function to \eppairs &$\ElRel$ & \cref{fig:IRUniverse}& $\ElRel(A{\sqsubseteq}B) : \El\,A \distr{} \El\,B$ \\
Precision on terms& $\precision{A}{B}$& \cref{fig:IRUniverse} &  \\
Monotone translation of types &$\monTy{\cdot}$ & \cref{fig:monotone-translation} & \\
Monotone translation of terms & $\monTm{\cdot}$& \cref{fig:monotone-translation} & \\
Propositional precision & $\tcol{\Gamma} \caty \tcol{t} \precision{\tcol{T}}{\tcol{U}} \tcol{u}$&\cref{def:propositional-precision} & \\
$\omega$-continuous maps & $A \tocont B$ & \cref{sec:grad-non-term} & $A,B$ $\omega$-cpos \\
$\omega$-continuous \eppair & $A \distrcont{} B$ & \cref{sec:grad-non-term}& \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
% & & & \\
\hline
\end{tabular}
\end{center}
\newpage

\section{Complements on Elaboration and \CCIC}

This section gives an extended account of \cref{sec:gcic-to-ccic}. The structure is the same, and we refer to the main section when things are already spelled out there.

\subsection{\CCIC}

We state and prove a handful of standard, technical properties of \CCIC, that are useful in the next sections. They should not be very surprising, the main specific point here is their formulation in the bidirectional setting.

\begin{property}[Weakening]
If $\tcol{\Gamma} \vdash \tcol{t} \inferty \tcol{T}$ then $\tcol{\Gamma, \Delta} \vdash \tcol{t} \inferty \tcol{T}$, and similarly for the other typing judgments.
\end{property}

\begin{proof}
We show by (mutual) induction on the typing derivation the more general statement that if $\tcol{\Gamma, \Gamma'} \vdash \tcol{t} \inferty \tcol{T}$ then $\tcol{\Gamma, \Delta, \Gamma'} \vdash \tcol{t} \inferty \tcol{T}$. It is true for the base cases (including the variable), and we can check that all rules preserve it.
\end{proof}

\begin{property}[Substitution]
If $\tcol{\Gamma, x : A, \Delta} \vdash \tcol{t} \inferty \tcol{T}$ and $\tcol{\Gamma} \vdash \tcol{u} \checkty \tcol{A}$ then $\tcol{\Gamma, \Delta\subs{u}{x}} \vdash \tcol{t\subs{u}{x}} \inferty \tcol{S}$ with $\tcol{S} \conv \tcol{T\subs{u}{x}}$.
\end{property}

\begin{proof}
Again, the proof is by mutual induction on the derivation. In the checking judgment, we use the transitivity of conversion to conclude. In the constrained inference, we need injectivity of type constructors, which is a consequence of confluence.
\end{proof}

\begin{property}[Validity]
\label{prop:validity}
If $\tcol{\Gamma} \vdash \tcol{t} \inferty \tcol{T}$ and $\vdash \tcol{\Gamma}$, then $\tcol{\Gamma} \vdash \tcol{T} \pcheckty{[]} \tcol{[]_i}$ for some $i$.
\end{property}

\begin{proof}
Once again, this is a routine induction on the inference derivation, using subject reduction to handle the reductions in the constrained inference rules, to ensure that the reduced type is still well-formed. The hypothesis of context well-formedness is needed for the base case of a variable, to get that the type obtained from the context is indeed well-typed.
\end{proof}

\subsection{Precision and Reduction}
\label{sec:precision-reduction}

\paragraph{Structural lemmas} Let us start our lemmas by counterparts to the weakening and substitution lemmas for precision.

\begin{lemma}[Weakening of precision]
If $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$, then $\tcol{\GG, \DD} \vdash \tcol{t} \capre \tcol{t'}$ for any $\tcol{\DD}$.
\end{lemma}

\begin{proof}
This is by induction on the precision derivation, using weakening of \CCIC to handle the uses of typing.
\end{proof}

\begin{lemma}[Substitution and precision]
If $\tcol{\GG, x : S \mid S', \DD} \vdash \tcol{t} \capre \tcol{t'}$, $\tcol{\GG} \vdash \tcol{u} \capre \tcol{u'}$, $\tcol{\fs{\GG}} \vdash \tcol{u} \checkty \tcol{S}$ and $\tcol{\sn{\GG}} \vdash \tcol{u'} \checkty \tcol{S'}$ then $\tcol{\GG, \DD\subs{u \mid u'}{x}} \vdash \tcol{t\subs{u}{x}} \capre \tcol{t'\subs{u'}{x}}$.
\end{lemma}

\begin{proof}
The substitution property follows from weakening, again by induction on the precision derivation. Weakening is used in the variable case where $x$ is replaced by $u$ and $u'$, and the substitution property of \CCIC appears to handle the uses of typing.
\end{proof}

\paragraph{Catch-up lemmas}
With these structural lemmas at hand, let us turn to the proofs of the catch-up lemmas.

%\begin{lemma}[Universe catch-up]
%	\label{lem:catchup-univ-annex}
%	Under the hypothesis that $\tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$, if $\tcol{\GG} \vdash \tcol{[]_i} \cdpre T'$ and $\sn{\GG} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_{j}}$, then $\tcol{T'} \rtred \tcol{\?_{[]_{j}}}$ and $i + 1 \leq j$ or $\tcol{T'} \rtred \tcol{[]_i}$.

\begin{proof}[Proof of \cref{lem:catchup-univ}]
We want to prove the following: under the hypothesis that $\tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$, if $\tcol{\GG} \vdash \tcol{[]_i} \cdpre \tcol{T'}$ and $\tcol{\sn{\GG}} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_{j}}$, then either $\tcol{T'} \rtred \tcol{\?_{[]_{j}}}$ with $i + 1 \leq j$, or $\tcol{T'} \rtred \tcol{[]_i}$.

The proof is by induction on the precision derivation, mutually with the same property where $\cdpre$ is replaced by $\capre$.

Let us start with the proof for $\capre$. Using the precision derivation, we can decompose $\tcol{T'}$ into $\tcol{\cast{U_{n-1}}{S_n}{\dots \cast{U_1}{S_2}{T''}}}$, where the casts come from \nameref{infrule:capre-castr} rules, and $\tcol{T''}$ is either $\tcol{[]_i}$ (rule \nameref{infrule:capre-univ}) or $\tcol{?_{S}}$ for some $\tcol{S}$ (rule \nameref{infrule:capre-unk}), and we have $\tcol{\GG} \vdash \tcol{[]_{i+1}} \cdpre \tcol{S_k}$, $\tcol{\GG} \vdash \tcol{[]_{i+1}} \cdpre \tcol{T_k}$ and $\tcol{\GG} \vdash \tcol{[]_{i+1}} \cdpre \tcol{S}$.
By induction hypothesis, all of $\tcol{S_k}$, $\tcol{T_k}$ and $\tcol{S}$ reduce either to $\tcol{[]_{i+1}}$ or some $\tcol{\?_{[]_l}}$ with $i + 1 \leq l$. Moreover, because $\tcol{T'}$ type-checks against $\tcol{[]_j}$, we must have $\tcol{S_n} \conv \tcol{[]_j}$. This implies that $\tcol{S_n}$ cannot reduce to $\tcol{?_{[]_{l}}}$ by confluence, and thus it must reduce to $\tcol{[]_{i+1}}$.

Using that $i+1 \leq l$ and rules \nameref{redrule:down-unk}, \nameref{redrule:univ-univ} and \nameref{redrule:up-down} giving respectively
\begin{align*}
\tcol{\cast{?_{[]_l}}{X}{\?_{?_{[]_l}}}} &\redCCIC \tcol{\?_X} \\
\tcol{\cast{[]_{i+1}}{[]_{i+1}}{t}} &\redCCIC \tcol{t} \\
\tcol{\cast{?_{[]_{l}}}{X}{\cast{[]_{i+1}}{?_{[]_{l}}}{t}}} &\redCCIC \tcol{\cast{[]_{i+1}}{X}{t}}
\end{align*}
we can reduce away all casts. We thus get $\tcol{T'} \rtred \tcol{[]_i}$ or $\tcol{T'} \rtred \tcol{\?_{[]_{i+1}}}$, as expected.

For $\cdpre$, if $\tcol{\GG} \vdash \tcol{[]_i} \cdpre \tcol{T'}$ then by decomposing the precision derivation there is an $\tcol{S'}$ such that $\tcol{T'} \rtred \tcol{S'}$, $\tcol{\GG} \vdash \tcol{[]_i} \capre \tcol{S'}$, and by subject reduction $\tcol{\fs{\GG}} \vdash \tcol{S'} \pcheckty{[]} \tcol{[]_j}$. By induction hypothesis, either $\tcol{S'} \rtred \tcol{[]_i}$ or $\tcol{S'} \rtred \tcol{?_{[]_{i+1}}}$, and composing both reductions we get the desired result.
\end{proof}

%\begin{lemma}[Type catch-up]
%	\label{lem:catchup-type-long}
%	We have the following property, under the hypothesis that $\tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$:
%	\begin{enumerate}
%		\item if $\GG \vdash \tcol{\?_{[]_i}} \cdpre T'$ and $\sn{\GG} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_{j}}$, then $\tcol{T'} \rtred \tcol{\?_{[]_{j}}}$ and $i \leq j$;
%		\item if $\GG \vdash \tcol{\P x : A.B} \cdpre \tcol{T'}$, $\tcol{\fs{\GG}} \vdash \tcol{\P x : A. B} \inferty \tcol{[]_i}$ and $\sn{\GG} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_j}$ then $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ and $i \leq j$, or $\tcol{T'} \rtred \tcol{\P x : A' . B'}$ for some $\tcol{A'}$ and $\tcol{B'}$ such that $\GG \vdash \tcol{\P x : A . B} \cdpre \tcol{\P x :A' . B'}$;
%		\item if $\GG \vdash \tcol{I(\orr{a})} \cdpre \tcol{T'}$, $\tcol{\fs{\GG}} \vdash \tcol{I(\orr{a})} \inferty \tcol{[]_i}$ and $\sn{\GG} \vdash \tcol{T'} \pcheckty{[]} \tcol{[]_j}$ then $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ and $i \leq j$, or $\tcol{T'} \rtred \tcol{I(\orr{a'})}$ for some $\tcol{a'}$ such that $\GG \vdash \tcol{I(\orr{a})} \cdpre \tcol{I(\orr{a'})}$.
%	\end{enumerate}

\begin{proof}[Proof of \cref{lem:catchup-type}]