unique.tex

\section{Unique typing}\label{sec:unique}
There are a large number of ``natural'' properties about the typing and definitional equality judgments we will want to be true in order to reason that certain judgments are not derivable for ``obvious'' reasons, for example that it is not possible to prove $\vdash\P:\P$ (which is a necessary condition for soundness).

\begin{theorem}[Unique typing]\label{thm:unique}
If $\Gamma\vdash e:\alpha$ and $\Gamma\vdash e:\beta$, then $\Gamma\vdash\alpha\equiv\beta$.
\end{theorem}

Unfortunately, we cannot yet prove this theorem. The critical step is the Church-Rosser theorem, which we will develop in the next section. However, we can set up the induction, which is necessary now since the Church-Rosser theorem will require that this theorem is true, and we will be caught in a circularity unless we are careful about the claims.

We will prove this theorem by induction on the number of alternations between the judgments $\Gamma\vdash e:\alpha$ and $\Gamma\vdash\alpha\equiv\beta$ (which are mutually recursive). Define $\Gamma\vdash_n e:\alpha$ and $\Gamma\vdash_n\alpha\equiv\beta$ by induction on $n\in\N$ as follows:
\begin{itemize}
\item $\Gamma\vdash_0\alpha\equiv\beta$ iff $\alpha=\beta$.
\item $\Gamma\vdash_{n+1}\alpha\equiv\beta$ iff there is a proof of $\Gamma\vdash\alpha\equiv\beta$ using  only $\Gamma\vdash_n e:\alpha$ typing judgments.
\item Assuming $\Gamma\vdash_m\alpha\equiv\beta$ is defined for $m\le n$, $\Gamma\vdash_n e:\alpha$ means that there is a proof of $\Gamma\vdash e:\alpha$ in which all appeals to the conversion rule use $\Gamma\vdash_m\alpha\equiv\beta$ for $m\le n$.
\end{itemize}
So if $\Gamma\vdash_0 e:\alpha$, then there is a proof that does not use the conversion rule at all; if $\Gamma\vdash_1\alpha\equiv\beta$ then there is a proof whose typing judgments do not use the conversion rule; if $\Gamma\vdash_1 e:\alpha$ then there is a proof using only the $1$-provable conversion rule; and so on. We will prove \autoref{thm:unique} by induction on this $n$.

\begin{lemma}[$n$-provability basics]
\begin{thmlist}
\item If $m\le n$ then $\Gamma\vdash_m e:\alpha$ implies $\Gamma\vdash_n e:\alpha$.
\item If $m\le n$ then $\Gamma\vdash_m\alpha\equiv\beta$ implies $\Gamma\vdash_n \alpha\equiv\beta$.
\item If $\Gamma\vdash e:\alpha$ then $\Gamma\vdash_n e:\alpha$ for some $n\in\N$.
\item If $\Gamma\vdash\alpha\equiv\beta$ then $\Gamma\vdash_n \alpha\equiv\beta$ for some $n\in\N$.
\end{thmlist}
\end{lemma}
\begin{proof}
(1) is immediate from the definition, (2) follows from (1). (3,4) are proven by a mutual induction on the typing judgment.
\end{proof}
\begin{definition}
Say that $\vdash_n$ has \emph{definitional inversion} if the following properties hold:
\begin{enumerate}
\item If $\Gamma\vdash_n \U_\ell\equiv\U_{\ell'}$, then $\ell\equiv\ell'$.
\item If $\Gamma\vdash_n \forall x:\alpha.\;\beta\equiv\forall x:\alpha'.\;\beta'$, then $\Gamma\vdash_n \alpha\equiv\alpha'$ and $\Gamma,x:\alpha\vdash_n \beta\equiv \beta'$.
\item $\Gamma\vdash_n \U_\ell\not\equiv\forall x:\alpha.\;\beta$.
\end{enumerate}
(We will also use the term \emph{unique typing} for this property given \autoref{thm:utype}.) 
\end{definition}
There are other inversions along these lines, but distinguishing universes and foralls is the most important part and it is what we need for the induction.

\begin{theorem}[Unique typing]\label{thm:utype}
If $\vdash_n$ has definitional inversion, and $\Gamma\vdash_n e:\alpha$ and $\Gamma\vdash_n e:\beta$, then $\Gamma\vdash_n\alpha\equiv\beta$.
\end{theorem}
\begin{proof}
By the weakening lemma, we can use instead the judgment $\vdash'_n$ which has no weakening rule.

By induction on the proof of $\Gamma\vdash'_n e:\alpha$ with a secondary induction on $\Gamma\vdash'_n e:\beta$.
\begin{enumerate}
\item If $\Gamma\vdash'_n e:\alpha$ from the conversion rule on $\Gamma\vdash_n\alpha'\equiv\alpha$, $\Gamma\vdash_n e:\alpha'$, then $\Gamma\vdash_n\alpha'\equiv\beta$ by the IH, so $\Gamma\vdash_n\alpha\equiv\beta$ by transitivity. (Similarly if the conversion rule applies on $\Gamma\vdash'_n e:\beta$.)
\item Otherwise, the same typing rule applies in both derivations. The variable, universe, lambda, let, and constant cases are trivial.
\item In the forall case, we have $\Gamma\vdash_n\forall x:\alpha.\;\beta:\U_{\imax(\ell_1,\ell_2)},\U_{\imax(\ell_1',\ell_2')}$ from $\Gamma\vdash\alpha:\U_{\ell_1},\U_{\ell_1'}$ and $\Gamma\vdash\beta:\U_{\ell_2},\U_{\ell_2'}$, and from the inductive hypothesis $\Gamma\vdash_n\U_{\ell_1}\equiv\U_{\ell_1'}$. From definitional inversion, $\ell_1\equiv \ell_1'$ and $\ell_2\equiv \ell_2'$, so $\Gamma\vdash_n\U_{\imax(\ell_1,\ell_2)}\equiv\U_{\imax(\ell_1',\ell_2')}$.
\item In the application case, we have $\Gamma\vdash_n e_1\;e_2:\beta[e_2/x],\beta'[e_2/x]$ from $\Gamma\vdash_n e_1:\forall x:\alpha.\;\beta,\forall x:\alpha'.\;\beta'$ and $\Gamma\vdash_n e_2:\alpha,\alpha'$, and from the inductive hypothesis $\Gamma\vdash_n\forall x:\alpha.\;\beta\equiv\forall x:\alpha'.\;\beta'$. From definitional inversion, $\Gamma\vdash_n\alpha\equiv\alpha'$ and $\Gamma,x:\alpha\vdash_n\beta\equiv\beta'$, so $\Gamma\vdash_n\beta[e_2/x]\equiv\beta'[e_2/x]$.
\end{enumerate}
\end{proof}

Thus, it suffices to prove that $\vdash_n$ has definitional inversion for every $n$ to establish \autoref{thm:unique}. We can show the base case:
\begin{lemma}\label{thm:0dinv}
$\vdash_0$ has definitional inversion.
\end{lemma}
\begin{proof}
Since $\Gamma\vdash_0 e\equiv e'$ means $e=e'$, all cases are trivial by inversion on the construction of the term.
\end{proof}

\subsection{The $\kappa$ reduction}\label{sec:kappa}
\emph{Note: In this section, we will omit the indices from the provability relation, but we will focus on characterizing the $\equiv$ relation at a particular level. So read $\Gamma\vdash \alpha\equiv\beta$ as $\Gamma\vdash_{n+1} \alpha\equiv\beta$, and $\Gamma\vdash e:\alpha$ as $\Gamma\vdash_n e:\alpha$. Also (and importantly) we will assume that $\vdash_n$ has unique typing, which will prevent the appearance of certain pathologies.}

The standard formulation of the Church-Rosser theorem, when applied to the $\rightsquigarrow$ reduction relation, is not true; under reasonable definitions of reduction, Lean will not have unique normal forms, because of proof irrelevance. (We already saw how this plays out in \autoref{sec:undecidable}). All other substantive reduction rules act on terms the same way regardless of their types. To analyze this, we will split the definitional equality judgment into two parts: A $\beta\delta\zeta\iota$-reduction relation (henceforth abbreviated $\kappa$ reduction), and a relation that does proof irrelevance. The idea is that $\kappa$ reduction satisfies a modified version of the Church-Rosser theorem, while proof irrelevance picks up the pieces, quantifying exactly how non-unique the normal form is.

The $\eta$ rule can sometimes fight against the $\iota$ reduction in the sense that it is possible for a subsingleton eliminator to reduce in two ways, where the $\eta$ reduced form cannot reduce, for example with the following reductions, using $\rec_{a=}:\forall C.\;C\;a\to \forall b.\;a=b\to C\;b$:
\begin{align*}
&\lambda h:a=a.\;\rec_{a=}\;C\;e\;a\;h\rightsquigarrow_\eta\rec_{a=}\;C\;e\;a\\
&\lambda h:a=a.\;\rec_{a=}\;C\;e\;a\;h\rightsquigarrow_\iota\lambda h:a=a.\;e
\end{align*}

To resolve this, we will require that $\rec$ and $\lift$ always have their required number of parameters. To accomplish this, we define an $\eta$-expansion map as a preprocessing stage on terms before reduction. The transformation is as follows:
\begin{itemize}
\item If $e$ is a list of terms of length $n$ and $\rec_P$ has $m\ge n$ arguments, then $\overline{\rec_P\;e}=\lambda x::\alpha.\;\rec_P\;e\;x$ where $x$ is the remaining $n-m$ arguments, with type $\alpha$ according to the specification of $P$.
\item If $e$ is a list of terms of length $n\le 6$ (note that $\lift$ has 6 arguments), then $\overline{\lift\;e}=\lambda x::\alpha.\;\lift\;e\;x$ where $x$ is the remaining $6-n$ arguments.
\item Otherwise, the transformation is recursive in subterms: $\overline x=x$, $\overline{\lambda x:\alpha.\;e}=\lambda x:\overline{\alpha}.\;\overline{e}$, etc. 
\end{itemize}
A term is said to be in $\rec$-normal form if every $\rec_P$ and $\lift$ subterm is followed by a sequence of applications of the appropriate length.

\begin{lemma}[Properties of the $\rec$-normal form]
\begin{itemize}
\item A term $e$ is in $\rec$-normal form iff $\bar e=e$.
\item $\bar e$ is always in $\rec$-normal form.
\item If $\Gamma\vdash e:\alpha$, then $\Gamma\vdash \overline{e}\equiv e$. (In fact, the proof of equivalence uses only $\eta$.)
\item If $e_1,e_2$ are in $\rec$-normal form, then so is $e_1[e_2/x]$.
\end{itemize}
\end{lemma}

The $\kappa$ reduction relation is defined on terms in $\rec$-normal form, with compatibility rules such as these for every syntax operator (including $\rec_P\;e$ and $\lift\;e$):
$$\boxed{\Gamma\vdash e\rightsquigarrow_\kappa e'}\qquad
\frac{\Gamma\vdash e_1 \rightsquigarrow_\kappa e_1'}{\Gamma\vdash e_1\;e_2\rightsquigarrow_\kappa e_1'\;e_2}\qquad
\frac{\Gamma\vdash e_2 \rightsquigarrow_\kappa e_2'}{\Gamma\vdash e_1\;e_2\rightsquigarrow_\kappa e_1\;e_2'}$$
$$\frac{\Gamma\vdash \alpha \rightsquigarrow_\kappa\alpha'}{\Gamma\vdash \lambda x:\alpha.\;e\rightsquigarrow_\kappa \lambda x:\alpha'.\;e}\qquad
\frac{\Gamma,x:\alpha\vdash e \rightsquigarrow_\kappa e'}{\Gamma\vdash \lambda x:\alpha.\;e\rightsquigarrow_\kappa \lambda x:\alpha.\;e'}\qquad\dots$$
The substantive rules are:
$$(\beta)\ \frac{}{\Gamma\vdash (\lambda x:\alpha.\;e)\;e'\rightsquigarrow_\kappa e[e'/x]}\qquad
(\delta)\ \frac{\mathsf{def}\;c:\alpha:=e}{\Gamma\vdash c\rightsquigarrow_\kappa e}\qquad
(\zeta)\ \frac{}{\Gamma\vdash \elet{x:\alpha:=e'}{e}\rightsquigarrow_\kappa e[e'/x]}$$
$$(\iota)\ \frac{P\mbox{ is non-SS inductive with ctor }c}{\Gamma\vdash \rec_P\;C\;e\;p\;(c\;b)\rightsquigarrow_\kappa e_c\;b\;v}\qquad
(\iota_q)\ \frac{}{\Gamma\vdash \lift\;R\;f\;h\;(\mk_R\;a)\rightsquigarrow_\kappa f\;a}$$
$$(K^+)\ \frac{P\mbox{ is SS inductive}\quad\Gamma\vdash \intro\;\inv[p,h]:\alpha}{\Gamma\vdash \rec_P\;C\;e\;p\;h\rightsquigarrow_\kappa e\;\inv[p,h]\;v}$$

See \autoref{sec:inductive} for the variable names and types used in the $\iota$ rules; recall in particular that $v$ in the RHS of the rule is a sequence of lambdas $v_i=\lambda x::\xi_i.\;\rec_P\;C\;e\;\pi_i[b,x]\;(u_i\;x)$ dictated by the definition of the inductive type.

We have an alternate $\iota$ rule for SS inductives, where $\inv[p,h]$ is a sequence of terms such that $\intro\;\inv[p,h]\equiv h$ (by proof irrelevance) and $\inv_i[p,\intro\;b]\equiv b_i$, which we call $K^+$ because it is a souped-up version of the K-like reduction rule in \autoref{sec:iota}. It applies only when $\intro\;\inv[p,h]$ is well-typed (and is the reason why $\rightsquigarrow_\kappa$ needs a context), which can also be written as a collection of $\equiv$ judgments at $\vdash_n$.

By the definition of a subsingleton inductive, every argument to the $\intro$ constructor is either propositional, or appears as one of the parameters $p_i$ to the inductive family. We define $\inv_i[p,h]:=p_j$ when the $i$th constructor argument is non-propositional and appears at position $j$ in the output type, and $\inv_i[p,h]=\inv_i\;h$ for the propositions, where $\inv_i$ is an atomic projection function. These $\inv_i$ projection operators can be defined using the recursor, like we demonstrated for $\acc$ in \autoref{sec:undecidable}. It doesn't really matter if these terms reduce or not (i.e. they could be constants or defined via the recursor), since they are proofs and are thus going to be pushed into the proof irrelevance relation.

The proof irrelevance relation deals with all the ways that normal forms can fail to be unique. Specifically, this relation is responsible for changing universe levels and changing proofs, as well as the $\eta$ rule.
$$\boxed{\Gamma\vdash e\equiv_p e'}$$
$$\frac{\Gamma\vdash e:\alpha}{\Gamma\vdash e\equiv_p e}\qquad
\frac{\Gamma\vdash\alpha\equiv_p\alpha'\quad \Gamma,x:\alpha\vdash e\equiv_p e'}{\Gamma\vdash \lambda x:\alpha.\;e\equiv_p \lambda x:\alpha'.\;e'}\qquad
\frac{\Gamma\vdash e_1\equiv_p e_1'\quad \Gamma\vdash e_2\equiv_p e_2'}{\Gamma\vdash e_1\;e_2\equiv_p e_1'\;e_2'}\qquad\dots$$
$$\frac{\Gamma,x:\alpha\vdash e\equiv_p e'\;x}{\Gamma\vdash \lambda x:\alpha.\;e\equiv_p e'}\qquad
\frac{\Gamma,x:\alpha\vdash e\;x\equiv_p e'}{\Gamma\vdash e\equiv_p \lambda x:\alpha.\;e'}\qquad
\frac{\Gamma\vdash p:\P\quad \Gamma\vdash h:p\quad \Gamma\vdash h':p}{\Gamma \vdash h\equiv_p h'}$$
The ellipsis abbreviates all the compatibility rules. The $\eta$ rule here is split in two because $\equiv_p$ lacks a symmetry rule, but it is also tightly syntax-constrained -- it is essentially only useful for proving $\lambda x::\alpha.\;e\;x\equiv_p e$. In particular it does not apply at all on proving that two variables of function type are equivalent, or proving that two universes or non-function things are equivalent.

\begin{lemma}[Regularity of reductions]
\begin{thmlist}
\item If $\Gamma\vdash e:\alpha$ and $\Gamma\vdash e\rightsquigarrow_\kappa e'$, then $\Gamma\vdash e\equiv e':\alpha$.
\item $\equiv_p$ is an equivalence relation.
\item If $\Gamma\vdash e\equiv_p e'$, then $\Gamma\vdash e\equiv e'$.
\item\label{item:p_subst} If $\Gamma,x:\alpha\vdash e_1\equiv_p e_1'$ and $\Gamma\vdash e_2\equiv_p e_2'$ then $\Gamma\vdash e_1[e_2/x]\equiv_p e_1'[e_2'/x]$.
\end{thmlist}
\end{lemma}
\begin{proof}
All parts are easy inductions.
\end{proof}
Note that the first part implies subject reduction for $\rightsquigarrow_\kappa$.

\subsection{The Church-Rosser theorem}\label{sec:church_rosser}
\begin{theorem}[Church-Rosser property]\label{thm:church_rosser}
If $\Gamma\vdash e:\alpha$, and $e\rightsquigarrow_\kappa^* e_1$ and $e\rightsquigarrow_\kappa^* e_2$, then there exists $e_1'$ and $e_2'$ such that $\Gamma\vdash e_1'\equiv_p e_2'$, and $e_1\rightsquigarrow_\kappa^* e_1'$ and $e_2\rightsquigarrow_\kappa^* e_2'$.
\end{theorem}
The proof follows the Tait--Martin-L\"{o}f method, extended to all the $\kappa$ rules. Define the parallel reduction $\gg_\kappa$ by the following rules:
$$\frac{}{\Gamma\vdash x\gg_\kappa x}\qquad
\frac{\Gamma\vdash \alpha\gg_\kappa\alpha'\quad \Gamma,x:\alpha\vdash e\gg_\kappa e'}{\Gamma\vdash \lambda x:\alpha.\;e\gg_\kappa \lambda x:\alpha'.\;e'}\qquad
\frac{\Gamma\vdash e_1\gg_\kappa e_1'\quad \Gamma\vdash e_2\gg_\kappa e_2'}{\Gamma\vdash e_1\;e_2\gg_\kappa e_1'\;e_2'}\qquad\dots$$
$$\frac{\Gamma,x:\alpha\vdash e_1\gg_\kappa e_1'\quad \Gamma\vdash e_2\gg_\kappa e_2'}{\Gamma\vdash (\lambda x:\alpha.\;e_1)\;e_2\gg_\kappa e_1'[e_2'/x]}$$
$$\frac{\Gamma\vdash e_2[e_1/x]\gg_\kappa e'}{\Gamma\vdash \elet{x:\alpha:=e_1}{e_2}\gg_\kappa e'}\qquad
\frac{\mathsf{def}\;c:\alpha:=e\quad \Gamma\vdash e\gg_\kappa e'}{\Gamma\vdash c\gg_\kappa e'}$$
$$\frac{\Gamma\vdash f\gg_\kappa f'\quad \Gamma\vdash a\gg_\kappa a'}{\Gamma\vdash \lift\;R\;f\;h\;(\mk_R\;a)\gg_\kappa f'\;a'}\qquad
\frac{\begin{matrix}
P\mbox{ is non-SS inductive with ctor }c\\
\Gamma\vdash C,e,b,p\gg_\kappa C',e',b',p'
\end{matrix}}{\Gamma\vdash \rec_P\;C\;e\;p\;(c\;b)\gg_\kappa e'\;b'\;v'}$$
$$\frac{P\mbox{ is SS inductive}\quad\Gamma\vdash \intro\;\inv[p,h]:\alpha\quad\Gamma\vdash C,e,p,h\gg_\kappa C',e',p',h'}{\Gamma\vdash \rec_P\;C\;e\;p\;h\gg_\kappa e_c'\;\inv[p',h']\;v'}$$

The ellipsis on the first line abbreviates compatibility rules for all the term constructors, recursing into all subterms like in the examples for lambda and application. All the substantive rules also follow a similar pattern: for each substantive rule in $\rightsquigarrow_\kappa$, there is a corresponding rule where after applying the $\rightsquigarrow_\kappa$ rule all variables on the RHS are $\gg_\kappa$ evaluated to the primed versions, and these are what end up in the target expression. (Note that in the $\iota$ rule, $v$ is a term that mentions $e$ and $p$; these are replaced by the primed versions in $v'$.)

In addition, we define the following ``complete reduction'' $\Gamma\vdash e\ggg_\kappa e'$ by exactly the same rules as $\gg_\kappa$, except that the compatibility rules only apply if none of the substantive rules are applicable. This makes $\ggg_\kappa$ almost deterministic (producing a unique $e'$ given $e$), except that the $\equiv_p$ hypothesis in the $\iota$ rule allows some freedom of choice of the parameters $b$.

It is easy to prove the following properties by induction:
\begin{lemma}[Properties of $\gg_\kappa$]\label{thm:gg_prop}
\begin{thmlist}
\item If $\Gamma\vdash e:\alpha$, then $\Gamma\vdash e\gg_\kappa e$.
\item\label{item:red_gg} If $\Gamma\vdash e\rightsquigarrow_\kappa e'$ then $\Gamma\vdash e\gg_\kappa e'$.
\item\label{item:gg_red} If $\Gamma\vdash e\gg_\kappa e'$ then $\Gamma\vdash e\rightsquigarrow_\kappa^* e'$.
\item\label{item:gg_subst} If $\Gamma,x:\alpha\vdash e_1\gg_\kappa e_1'$ and $\Gamma\vdash e_2\gg_\kappa e_2'$ (where $\Gamma\vdash e_2:\alpha$) then\\ $\Gamma\vdash e_1[e_2/x]\gg_\kappa e_1'[e_2'/x]$.
\item\label{item:ggg_gg} If $\Gamma\vdash e\ggg_\kappa e'$, then $\Gamma\vdash e\gg_\kappa e'$.
\item\label{item:ggg_ex} If $\Gamma\vdash e:\alpha$, then $\Gamma\vdash e\ggg_\kappa e'$ for some $e'$.
\end{thmlist}
\end{lemma}

\begin{lemma}[Compatibility of $\gg_\kappa$ with $\equiv_p$]\label{thm:gg_compat}
If $\Gamma\vdash e_1\equiv_p e_3\gg_\kappa e_2$, then there exists $e_4$ such that $\Gamma\vdash e_1\gg_\kappa e_4\equiv_p e_2$.
\end{lemma}
\begin{proof}
By induction on $e_1\equiv_p e_3$ and inversion on $e_3\gg_\kappa e_2$. (We will omit the contexts from the relations.)
\begin{itemize}
\item If $e_1\equiv_p e_3=e_1$ by the reflexivity rule, then $e_1\gg_\kappa e_2\equiv_p e_2$.
\item If $e_1\equiv_p e_3$ by the proof irrelevance rule, then $e_3:p:\P$, so $e_2:p:\P$ as well and hence $e_1\gg_\kappa e_1\equiv_p e_2$.
\item If $e_1\equiv_p e_3$ and $e_3\gg_\kappa e_2$ both use the same compatibility rule, then it is immediate from the induction hypothesis.
\item If $e_1:p:\P$ is a proof, then $e_1\gg_\kappa e_1\equiv_p e_2$. (We will thus assume that $e_1$ is not a proof in later cases.)
\item If $(\lambda x:\alpha_1.\;e_1)\;e_1'\equiv_p(\lambda x:\alpha_3.\;e_3)\;e_3'\gg_\kappa e_2[e_2'/x]$ where $e_1\equiv_p e_3\gg_\kappa e_2$, $e_1'\equiv_p e_3'\gg_\kappa e_2'$ and $\alpha_1\equiv\alpha_3$, then $(\lambda x:\alpha_1.\;e_1)\;e_1'\gg_\kappa e_1[e_1'/x]\equiv_p e_2[e_2'/x]$. (Other cases are similar, when the $\equiv_p$ is proven by compatibility rules and the $\gg_\kappa$ is a substantive rule.)
\item If $e_1\;e_1'\equiv_p(\lambda x:\alpha_3.\;e_3)\;e_3'\gg_\kappa e_2[e_2'/x]$ where $e_1\;x\equiv_p e_2\gg_\kappa e_3$ and $e_1'\equiv_p e_2'\gg_\kappa e_3'$, then $e_1\;e_1'=(e_1\;x)[e_1'/x]\equiv_p e_2[e_2'/x]$.
\item If $\lift\;R_1\;\beta_1\;f_1\;h_1\;q_1\equiv_p\lift\;R_3\;\beta_3\;f_3\;h_3\;(\mk_R\;a_3)$ where $q_1\equiv_p \mk_R\;a_3$ by proof irrelevance, then $\beta:\P$ so $e_1:\beta$ is a proof. (Note: we are using that $\vdash_n$ has unique typing here.)
\item If $\rec_P\;C_1\;e_1\;p_1\;h_1\equiv_p\rec_P\;C_3\;e_3\;p_3\;(c\;b_3)\gg_\kappa (e_2)_c\;b_2\;v_2$ where $P$ is non-SS inductive and $h_1\equiv_p c\;b_3$ by proof irrelevance, it is a small eliminator, so $\rec_P\;C_1\;e_1\;p_1\;h_1$ is a proof.
\end{itemize}
\end{proof}
\begin{lemma}[Triangle lemma]\label{thm:tri}
If $\Gamma\vdash e:\alpha$, $e\gg_\kappa e'$, and $e\ggg_\kappa e^\bullet$, then there exists $e^\circ$ such that $\Gamma\vdash e'\gg_\kappa e^\circ\equiv_p e^\bullet$.
\end{lemma}
\begin{proof}
By induction on $e\ggg_\kappa e^\bullet$ and inversion on $e\gg_\kappa e'$.
\begin{itemize}
\item If $x\lll_\kappa x\gg_\kappa x$, then $x\gg_\kappa x\equiv_p x$.
\item If $e\ggg_\kappa e^\bullet$ by the beta rule:
\begin{itemize}
\item If $e_1^\bullet[e_2^\bullet/x]\lll_\kappa(\lambda x:\alpha.\;e_1)\;e_2\gg_\kappa e_1'[e_2'/x]$ by the beta rule, then $e_1'\gg_\kappa e_1^\circ$ and $e_2'\gg_\kappa e_2^\circ$ by the inductive hypothesis, so $e_1'[e_2'/x]\gg_\kappa e_1^\circ[e_2^\circ/x]\equiv_p e_1^\bullet[e_2^\bullet/x]$ by the substitution property.
\item If $e_1^\bullet[e_2^\bullet/x]\lll_\kappa(\lambda x:\alpha.\;e_1)\;e_2\gg_\kappa (\lambda x:\alpha.\;e_1')\;e_2'$ by the application rule and lambda rule, then $(\lambda x:\alpha.\;e_1')\;e_2'\gg_\kappa e_1^\circ[e_2^\circ/x]\equiv_p e_1^\bullet[e_2^\bullet/x]$ by the beta rule for $\gg_\kappa$ and the IH.
\end{itemize}
\item If $e^\bullet\lll_\kappa c\gg_\kappa e'$ by the delta rule, then $e'\gg_\kappa e^\circ\equiv_p e^\bullet$.
\item If $e_1^\bullet[e_2^\bullet/x]\lll_\kappa\elet{x:\alpha:=e_1}{e_2}\gg_\kappa e_2'[e_1'/x]$ by the zeta rule, then $e_1'[e_2'/x]\gg_\kappa e_1^\circ[e_2^\circ/x]\equiv_p e_1^\bullet[e_2^\bullet/x]$.
\item If $e\ggg_\kappa e^\bullet$ by the non-SS inductive iota rule:
\begin{itemize}
\item If $e_c^\bullet\;b^\bullet\;v^\bullet\lll_\kappa \rec_P\;C\;e\;p\;(c\;b)\gg_\kappa e_c'\;b'\;v'$ by the iota rule, then $e_c'\;b'\;v'\gg_\kappa e_c^\circ\;b^\circ\;v^\circ\equiv_p e_c^\bullet\;b^\bullet\;v^\bullet$.
\item If $e_c^\bullet\;b^\bullet\;v^\bullet\lll_\kappa \rec_P\;C\;e\;p\;(c\;b)\gg_\kappa \rec_P\;C'\;e'\;p'\;(c\;b')$ by the $\rec_P$ compatibility rule, then $\rec_P\;C'\;e'\;p'\;(c\;b')\gg_\kappa e_c^\circ\;b^\circ\;v^\circ\equiv_p e_c^\bullet\;b^\bullet\;v^\bullet$ by the iota rule.
\end{itemize}
\item If $e\ggg_\kappa e^\bullet$ by the quotient iota rule:
\begin{itemize}
\item If $f^\bullet\;a^\bullet\lll_\kappa \lift\;R\;f\;h\;(\mk_R\;a)\gg_\kappa f'\;a'$ by the iota rule, then $f'\;a'\gg_\kappa f^\circ\;a^\circ\equiv_p f^\bullet\;a^\bullet$.
\item If $f^\bullet\;a^\bullet\lll_\kappa \lift\;R\;f\;h\;(\mk_R\;a)\gg_\kappa\lift\;R'\;f'\;h'\;(\mk_{R'}\;a')$ by the $\lift$ compatibility rule, then we have $q'\gg_\kappa q^\circ\equiv_p q^\bullet$ for $q\in\{C,e,p,h\}$, and $\lift\;R'\;f'\;h'\;(\mk_{R'}\;a')\gg_\kappa f^\circ\;a^\circ\equiv_p f^\bullet\;a^\bullet$.
\end{itemize}
\item If $e\ggg_\kappa e^\bullet$ by the $K^+$ rule:
\begin{itemize}
\item If $e_c^\bullet\;\inv[p^\bullet,h^\bullet]\;v^\bullet\lll_\kappa \rec_P\;C\;e\;p\;h\gg_\kappa e_c'\;\inv[p',h']\;v'$ by the iota rule, then\\
$e_c'\;\inv[p',h']\;v'\gg_\kappa e_c^\circ\;\inv[p^\circ,h^\circ]\;v^\circ\equiv_p e_c^\bullet\;\inv[p^\bullet,h^\bullet]\;v^\bullet$.
\item If $e_c^\bullet\;\inv[p^\bullet,h^\bullet]\;v^\bullet\lll_\kappa \rec_P\;C\;e\;p\;h\gg_\kappa \rec_P\;C'\;e'\;p'\;h'$ by the $\rec_P$ compatibility rule, then $\rec_P\;C'\;e'\;p'\;h'\gg_\kappa e_c^\circ\;\inv[p^\circ,h^\circ]\;v^\circ\equiv_p e_c^\bullet\;\inv[p^\bullet,h^\bullet]\;v^\bullet$ by the iota rule.
\end{itemize}
\item If $e\ggg_\kappa e^\bullet$ by a compatibility rule:
\begin{itemize}
\item If $e_1^\bullet\;e_2^\bullet\lll_\kappa e_1\;e_2\gg_\kappa e_1'\;e_2'$ by the application rule, then $e_1'\;e_2'\gg_\kappa e_1^\circ\;e_2^\circ\equiv_p e_1^\bullet\;e_2^\bullet$.
\item If $\forall x:\alpha^\bullet.\;e^\bullet\lll_\kappa \forall x:\alpha.\;e\gg_\kappa \forall x:\alpha'.\;e'$ by the forall rule, then $\forall x:\alpha'.\;e'\gg_\kappa \forall x:\alpha^\circ.\;e^\circ\equiv_p \forall x:\alpha^\bullet.\;e^\bullet$.
\item Other compatibility rules follow the same pattern.
\end{itemize}
\end{itemize}\vspace{-6mm}
\end{proof}
The main proof of Church-Rosser is a corollary of \autoref{thm:tri}, and does not differ substantially from the usual proof putting diamonds together, because the additional complication of having $\equiv_p$ at the bottom of the diamond commutes with all the other reductions.
\begin{proof}[Proof of \autoref{thm:church_rosser}]
We prove in succession the following theorems:
\begin{enumerate}
\item If $\Gamma\vdash e:\alpha$, and $e_1\ll_\kappa e\gg_\kappa e_2$, then $\exists e_1'\;e_2'.\; e_1\gg_\kappa e_1'\equiv_p e_2'\ll_\kappa e_2$.
\item If $\Gamma\vdash e:\alpha$, and $e_1\ll_\kappa^* e\gg_\kappa e_2$, then $\exists e_1'\;e_2'.\; e_1\gg_\kappa e_1'\equiv_p e_2'\ll_\kappa^* e_2$.
\item If $\Gamma\vdash e:\alpha$, and $e_1\ll_\kappa^* e\gg_\kappa^* e_2$, then $\exists e_1'\;e_2'.\; e_1\gg_\kappa^* e_1'\equiv_p e_2'\ll_\kappa^* e_2$.
\item If $\Gamma\vdash e:\alpha$, and $e_1\leftsquigarrow_\kappa^*e\rightsquigarrow_\kappa^* e_2$, then $\exists e_1'\;e_2'.\; e_1\rightsquigarrow_\kappa^* e_1'\equiv_p e_2'\leftsquigarrow_\kappa^* e_2$.
\end{enumerate}
(4) is the theorem we want.
\begin{enumerate}
\item If $e\gg_\kappa e_1,e_2$, then by \autoref{thm:tri} there exists $e_1',e_2'$ such that $e_i\gg_\kappa e_i'$ and $e_1'\equiv_p e^\bullet\equiv_p e_2'$. But then $e_1'\equiv_p e_2'$ are as desired. 
\item By induction on $e\gg_\kappa^* e_1$. If $e\gg_\kappa^* e_1\gg_\kappa e_3$ and we have inductively that $e_1\gg_\kappa e_1'\equiv_p e_2'\ll_\kappa^* e_2$, then by applying (1) to $e_3\ll_\kappa e_1\gg_\kappa e_1'$ we obtain $e_3\gg_\kappa e_3'\equiv_p e_1''\ll_\kappa e_1'$, and by \autoref{thm:gg_compat} applied to $e_1''\ll_\kappa e_1'\equiv_p e_2'$ we obtain $e_1''\equiv_p e_2''\ll_\kappa e_2'$ so that  $e_3\gg_\kappa e_3'\equiv_p e_1''\equiv_p e_2''\ll_\kappa e_2'\ll_\kappa^* e_2$.
\item By induction on $e\gg_\kappa^* e_2$. The proof is the same as (2), replacing \autoref{thm:gg_compat} for the analogous statement for $\gg_\kappa^*$, i.e. if $e_1\gg_\kappa^*e_2$ and $e_1\equiv_p e_1'$ then there exists $e_2'$ such that $e_1'\gg_\kappa^*e_2'\equiv_p e_1'$. This follows by induction on \autoref{thm:gg_compat}.
\item  The equivalence of (3) and (4) comes from properties \ref{item:red_gg} and \ref{item:gg_red}.
\end{enumerate}
\end{proof}

Now say that $\Gamma\vdash e_1\equiv_\kappa e_2$ if $\Gamma\vdash e_1,e_2:\alpha$ for some $\alpha$, and there exists $e_1',e_2'$ such that $\Gamma\vdash e_1\rightsquigarrow_\kappa^* e_1'\equiv_p e_2'\leftsquigarrow_\kappa^* e_2$. This relation is obviously reflexive and symmetric and implies $\Gamma\vdash e_1\equiv e_2$, and the Church-Rosser property implies it is also transitive.

\begin{theorem}[Completeness of the $\kappa$ reduction]\label{thm:ckappa}
$\Gamma\vdash e\equiv e'$ if and only if $\Gamma\vdash e\equiv_\kappa e'$.
\end{theorem}
\begin{proof}
The reverse direction follows from regularity lemmas observed above. The forward direction is by induction on $\equiv$.
\begin{itemize}
\item The equivalence relation rules are immediate since $\equiv_\kappa$ is an equivalence relation (by the Church-Rosser property).
\item For the compatibility rules, since both $\equiv_p$ and $\rightsquigarrow_\kappa$ have compatibility rules, this property passes to $\equiv_\kappa$. Thus, for example in the lambda case, we have $\Gamma\vdash\lambda x:\alpha.\;e\equiv_\kappa\lambda x:\alpha.\;e'$ since $\Gamma,x:\alpha\vdash e\equiv_\kappa e'$ from the IH, and similarly $\Gamma\vdash\lambda x:\alpha.\;e'\equiv_\kappa\lambda x:\alpha'.\;e'$, so by transitivity $\Gamma\vdash\lambda x:\alpha.\;e\equiv_\kappa\lambda x:\alpha'.\;e'$.
\item The universe changing rules (for constants and $\U_\ell$) are in $\equiv_p$.
\item The $\beta$ and $\eta$ rules are in $\rightsquigarrow_\kappa$, and the proof irrelevance rule is in $\equiv_p$. All the other equivalence rules are also introduced in $\rightsquigarrow_\kappa$.
\item For subsingleton eliminators, we must show $\rec_P(C,e,p,\intro\;b)\equiv_\kappa e\;b\;v$. From the $K^+$ rule we have $\rec_P(C,e,p,\intro\;b)\equiv_\kappa e\;\inv[p,c\;b]\;v$ so it suffices to show $\inv_i[p,\intro\;b]\equiv_\kappa b_i$ for each $i$. If $b_i$ is propositional then this is by proof irrelevance, otherwise $\inv_i[p,\intro\;b]=p_j$, and the well-typedness of $\rec_P(C,e,p,\intro\;b)$ implies that $\Gamma\vdash_n b_i\equiv p_j$. Thus by completeness of the $\kappa$ reduction at $\vdash_n$, $\Gamma\vdash_n b_i\equiv_\kappa p_j$ and hence $\Gamma\vdash_{n+1} b_i\equiv_\kappa p_j$.
\end{itemize}
\end{proof}

Now we can finally finish the inductive step of the proof of \autoref{thm:unique}:

\begin{theorem}[Definitional inversion]\label{thm:1dinv}
$\vdash_{n+1}$ has definitional inversion.
\end{theorem}
\begin{proof}
In each case we apply \autoref{thm:ckappa} on the assumptions.
\begin{enumerate}
\item \emph{If $\Gamma\vdash_{n+1} \U_\ell\equiv\U_{\ell'}$, then $\ell\equiv\ell'$.}

Again, there are no $\rightsquigarrow_\kappa$ reductions from $\U_\ell$, so $\Gamma\vdash_{n+1} \U_\ell\equiv_p\U_{\ell'}$, and if the compatibility rule is used then $\ell\equiv\ell'$. If proof irrelevance is used, then $\Gamma\vdash_n\U_\ell,\U_{\ell'}:p$ for some $\Gamma\vdash_n p:\P$. Since $\Gamma\vdash_n\U_\ell:\U_{S\ell}:\U_{SS\ell}$ as well, by unique typing at $n$, $\Gamma\vdash_n \P\equiv \U_{SS\ell}$, so by definitional inversion $0\equiv SS\ell$, a contradiction.

\item \emph{If $\Gamma\vdash_{n+1} \forall x:\alpha.\;\beta\equiv\forall x:\alpha'.\;\beta'$, then $\Gamma\vdash_{n+1} \alpha\equiv\alpha'$ and $\Gamma,x:\alpha\vdash_{n+1} \beta\equiv \beta'$.}

In this case, there are no $\rightsquigarrow_\kappa$ reductions except the compatibility rules, so $\forall x:\alpha.\;\beta\rightsquigarrow_\kappa^*\forall x:\alpha_1.\;\beta_1$ for some $\alpha\rightsquigarrow_\kappa^*\alpha_1$ and $\beta\rightsquigarrow_\kappa^*\beta_1$, and similarly $\alpha'\rightsquigarrow_\kappa^*\alpha'_1$ and $\beta'\rightsquigarrow_\kappa^*\beta'_1$, and if these are $\equiv_p$ equivalent using the compatibility rule then we are done.

If $\Gamma\vdash_{n+1}\forall x:\alpha_1.\;\beta_1\equiv_p\forall x:\alpha'_1.\;\beta'_1$ by proof irrelevance, then $\Gamma\vdash_n\forall x:\alpha_1.\;\beta_1,\forall x:\alpha'_1.\;\beta'_1:p:\P$. But $\Gamma\vdash_n\forall x:\alpha_1.\;\beta_1:\U_{\imax(\ell_1,\ell_2)}$ for some $\ell_1,\ell_2$ since $\alpha_1$ and $\beta_1$ are well-typed, so by unique typing at $n$, $p\equiv\U_{\imax(\ell_1,\ell_2)}$ and $0\equiv S\imax(\ell_1,\ell_2)$, a contradiction.

\item \emph{$\Gamma\vdash_n \U_\ell\not\equiv\forall x:\alpha.\;\beta$.}

Suppose not. Similarly to previous parts, as there are no reductions from $\U_\ell$ and no reductions except the compatibility rule for $\forall$, we obtain $\Gamma\vdash_n\U_\ell\equiv_p\forall x:\alpha'.\;\beta'$, and now there is no applicable rule except proof irrelevance, but this implies $\U_\ell:p:\P$ and hence $0\equiv SS\ell$, a contradiction.
\end{enumerate}
\end{proof}

We've already described the structure of this theorem in earlier parts, but now we are finally ready to put all the parts together:

\begin{proof}[Proof of \autoref{thm:unique}]
We prove by induction on $n$ that $\vdash_n$ has definitional inversion (and hence unique typing, by \autoref{thm:utype}), and also that it satisfies the conclusion of \autoref{thm:ckappa}.
\begin{itemize}
\item For $n=0$, $\vdash_0$ has definitional inversion by \autoref{thm:0dinv}, and \autoref{thm:ckappa} is trivial (where both $\Gamma\vdash e\equiv_\kappa e'$ and $\Gamma\vdash e\equiv e'$ mean $e=e'$).
\item For $n+1$, suppose $\vdash_n$ has definitional inversion and satisfies \autoref{thm:ckappa}. Then all the results of \autoref{sec:church_rosser} follow, including \autoref{thm:ckappa}. Then definitional inversion at $n+1$ is \autoref{thm:1dinv}.
\end{itemize}
\end{proof}