+ $\mytyp_l$ is replaced by $\mytyp$. \\
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \\
+ & | & \myprdec{\myprsyn} \mysynsep
+ \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
+ \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
+ & | & \mytmsyn \myeq \mytmsyn \mysynsep
+ \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+
+ There is only $\mytyp$, which corresponds to $\mytyp_0$. \\ Thus all
+ the type-formers take $\mytyp$ arguments and form a $\mytyp$. \\ \ \\
+
+ % TODO insert large eliminator
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+ \DisplayProof
+}
+
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+ \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+ \noLine
+ \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
+ \BinaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjud{\mytmm}{\myse{A}}$}
+ \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
+ \AxiomC{$\myjud{\mytmn}{\myse{B}}$}
+ \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+ \DisplayProof
+}
+
+\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{\ }c@{\ }l}
+ \myprdec{\mybot} & \myred & \myempty \\
+ \myprdec{\mytop} & \myred & \myunit
+ \end{array}
+ $
+ &
+ $
+ \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
+ \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
+ \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
+ \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
+ \end{array}
+ $
+ \end{tabular}
+}
+
+\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
+ $
+ \begin{array}{c@{\ }c@{\ }c@{\ }l}
+ \myempty & \myeq & \myempty & \myred \mytop \\
+ \myunit & \myeq & \myunit & \myred \mytop \\
+ \mybool & \myeq & \mybool & \myred \mytop \\
+ \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \\
+ \multicolumn{4}{l}{
+ \myind{2} \mytya_1 \myeq \mytyb_1 \myand
+ \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1 \myeq \mytyb_2}
+ } \\
+ \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+ \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+ \mytya & \myeq & \mytyb & \myred \mybot\ \text{for other canonical types.}
+ \end{array}
+ $
+}
+
+\mydesc{reduction}{\mytmsyn \myred \mytmsyn}{