% !TeX root = slides.tex
\section{Conclusion}

\begin{frame}{Overall Summary}
	\structure{Logical Relations:}
	\begin{itemize}
		\item many type theories admit this proof technique:\begin{enumerate}
			\item map every type $\tpName$ to an $n$-ary relation $C_{\tpName}(-)$
			\item prove that every constructor $f\colon\tpName_1\to\ldots\to\tpName_n\to\tpName$ preserves the relation $C_{\tpName}(-)$
		\end{enumerate}
		\item ``the basic lemma'': if $t\colon\tpName$, then $C_{\tpName}(t)$
	\end{itemize}
	\medskip

	\structure{Concretely in \mmt/LF:} for morphisms $\mu_1,\ldots,\mu_n\colon S \to T$
	\[
		\logrel{r}{\mu_1 \times \cdots \times \mu_n}{S}{T}
	\]
	\vspace{-1.5em}
	\begin{itemize}
		\item special case for morphisms being identities: \begin{itemize}
			\item $\nakedLogRel{\TND}{\id{PL}}{\PL}{\PL}$: unary congruence proving $p\colon\prop \Longrightarrow\;\vtnd{p}$
			\item $\nakedLogRel{\LRA}{\id{PL}\times\id{\PL}}{\PL}{\PL}$: (binary) congruence whose well-typedness shows $\Leftrightarrow$ being a congruence
		\end{itemize}
		%
		\item special case
		\vspace{-0.5em} \[
			\logrel{\TypePres}{\TypeEras}{\ChurchProd}{\CurryProd}
		\]
		\vspace*{-1em}
		\begin{itemize}
			\item complements lossy translation $\TypeEras$
			\item $\vdash_{\ChurchProd} t \colon \ttm{A} \;\;\Longrightarrow\;\;\vdash_{\CurryProd} \wit\colon\ofType{\TypeEras(t)}{\TypeEras(A)}$
		\end{itemize}
	\end{itemize}
\end{frame}
\begin{frame}{Future Work}
	\ldots
\end{frame}