paper: add type equivalence

paper/main.tex

@@ -333,29 +333,120 @@ in an expression \(e \in \nonterm{E} \) with the \(\psi_e(\metavariable{x_i})\)
 \end{definition}
 
 \subsection{Typing}
+
 \subsubsection{Equivalence of Type Terms}
 
-\begin{definition}[Distributivity]
+%We want distributivity of ladders over type-specialization as well as over function/morphism types.
-\todo{}
+\begin{definition}[Distributivity in Types]
 
+\begin{mathpar}
+\typeterminal{< \metavariable{\sigma}\sim\metavariable{\sigma'} \quad \metavariable{\tau} >}
+\rightarrow_\text{distribute}
+\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau} > \sim < \metavariable{\sigma'} \quad \metavariable{\tau} > }
+
+\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau}\sim\metavariable{\tau'} >}
+\rightarrow_\text{distribute}
+\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau} > \sim < \metavariable{\sigma} \quad \metavariable{\tau'} > }
+
+\typeterminal{ \metavariable{\sigma}\sim\metavariable{\sigma'} \rightarrow \metavariable{\tau} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow \metavariable{\tau} ) \sim ( \metavariable{\sigma'} \rightarrow \metavariable{\tau} ) }
+
+\typeterminal{ \metavariable{\sigma} \rightarrow \metavariable{\tau}\sim\metavariable{\tau'} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow \metavariable{\tau} ) \sim ( \metavariable{\sigma} \rightarrow \metavariable{\tau'} ) }
+
+\typeterminal{ \metavariable{\sigma}\sim\metavariable{\sigma'} \rightarrow_\text{morph} \metavariable{\tau} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau} ) \sim ( \metavariable{\sigma'} \rightarrow_\text{morph} \metavariable{\tau} ) }
+
+\typeterminal{ \metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau}\sim\metavariable{\tau'} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau} ) \sim ( \metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau'} ) }
+
+\end{mathpar}
+
+
+Let \(\rightarrow_\text{condense}\) be the inverse to \(\rightarrow_\text{distribute}\).
 
 See \hyperref[coq:type-dist]{equiv.v:\ref{coq:type-dist}}.
 \end{definition}
 
-\begin{definition}[Equivalence Relation]
+\begin{definition}[Alpha Conversion in Types]
-\todo{}
+\begin{mathpar}
+\typeterminal{\forall \metavariable{\alpha} . \metavariable{\tau}}
+\rightarrow_{\alpha}
+\typeterminal{\forall \metavariable{\alpha'} . } \{ \metavariable{\alpha} \mapsto \metavariable{\alpha'} \} \metavariable{\tau}
 
+\end{mathpar}
+\end{definition}
+
+\begin{definition}[Equivalence Relation]
+Transitive closure over \(\rightarrow_\text{distribute}\), \(\rightarrow_\text{condense}\) and \(\rightarrow_\alpha\).
+
+
+\begin{mathpar}
+
+\inferrule[E-Refl]{
+	\metavariable{\tau} \in \nonterm{T}
+}{
+	\metavariable{\tau} \equiv \metavariable{\tau}
+}\and
+\inferrule[E-Trans]{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}\\
+	\metavariable{\tau_2} \equiv \metavariable{\tau_3}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_3}
+}
+
+\inferrule[E-Rename]{
+	\metavariable{\tau_1} \rightarrow_\alpha \metavariable{\tau_2}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}
+
+\inferrule[E-Distribute]{
+	\metavariable{\tau_1} \rightarrow_\text{distribute} \metavariable{\tau_2}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}\and
+\inferrule[E-Condense]{
+	\metavariable{\tau_1} \rightarrow_\text{condense} \metavariable{\tau_2}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}
+
+\end{mathpar}
 
 See \hyperref[coq:type-equiv]{equiv.v:\ref{coq:type-equiv}}.
 \end{definition}
 
+
+\begin{lemma}[Symmetry of \(\equiv\)]
+
+\begin{mathpar}
+\inferrule[E-Symm]{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}{
+	\metavariable{\tau_2} \equiv \metavariable{\tau_1}
+}
+\end{mathpar}
+
+\begin{proof}
+\(\rightarrow_{distribute}\) is the inverse of \(\rightarrow_{condense}\) and \(\rightarrow_{\alpha}\) is symmetric by itself.
+\end{proof}
+
+\end{lemma}
+
 \subsubsection{Normal Forms}
 
 \begin{definition}[Ladder Normal Form]
-\todo{}
+LNF is reached by exhaustive application of \(\rightarrow_\text{distribute}\).
 \end{definition}
 
-\subsubsection{Subtyping}
+\begin{definition}[Parameter Normal Form]
+PNF reached by exhaustive application of \(\rightarrow_\text{condense}\).
+\end{definition}
 
 \begin{definition}[Syntactic Subtyping]
 \todo{}