+Where is $\myprop$ placed in the type hierarchy? The main indicator
+is the decoding operator, since it converts into things that already
+live in the hierarchy. For example, if we
+have {\mysmall\[
+ \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
+ \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
+ \]} we will better make sure that the `to be decoded' is at the same
+level as its reduction as to preserve subject reduction. In the example
+above, we'll have that proposition to be at least as large as the type
+of $\mynat$, since the reduced proof will abstract over it. Pretending
+that we had explicit, non cumulative levels, it would be tempting to have
+\begin{center}
+\begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
+ \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
+ \DisplayProof
+&
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
+ \DisplayProof
+\end{tabular}
+\end{center}
+$\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
+following rules similar to the ones for $\myprod$ and $\myarr$ in
+section \ref{sec:itt}. However, we need to be careful with value
+equality since for example we have that {\mysmall\[
+ \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
+ \myred
+ \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
+ \]} where the proposition decodes into something of type
+ $\mytyp_l$, where $\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We
+ can resolve this tension by making all equalities larger:
+\begin{prooftree}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytmn}{\mytyb}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
+\end{prooftree}
+This is disappointing, since type equalities will be needlessly large:
+$\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
+
+However, considering that our theory is cumulative, we can do better.
+Assuming rules for $\myprop$ cumulativity similar to the ones for
+$\mytyp$, we will have (with the conversion rule reproduced as a
+reminder):
+\begin{center}
+ \begin{tabular}{cc}
+ \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivspp
+
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytmn}{\mytyb}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
+ \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
+ \DisplayProof
+\end{center}
+
+That is, we are small when we can (type equalities) and large otherwise.
+This would not work in a non-cumulative theory because subject reduction
+would not hold. Consider for instance {\mysmall\[
+ \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
+ : \myprop_1
+\]}
+which reduces to
+{\mysmall\[
+ \myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0
+ \]} We need $\myprop_0$ to be $\myprop_1$ too, which will be the case
+with cumulativity. This is not the most elegant of systems, but it buys
+us a cheap type level equality without having to replicate functionality
+with a dedicated construct.
+
+\subsubsection{Quotation and term equality}
+\label{sec:kant-irr}
+
+% \begin{figure}[t]
+% \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
+
+% }
+% \caption{Quotation in \mykant.}
+% \label{fig:kant-quot}
+% \end{figure}