bsc-leon-vatthauer/slides/sections/02_goals.tex

\section{Implementation in Agda}

\begin{frame}[t, fragile]{Goals}
  \begin{itemize}[<+->]
    \item Formalize the delay monad categorically and show that it is..
    \begin{itemize}
      \item strong
      \item commutative
    \end{itemize}
    \item Formalize K and show that it is..
    \begin{itemize}
      \item strong
      \item commutative
      \item an equational lifting monad
      \item the initial pre-Elgot monad
    \end{itemize}
    \item Take the category of setoids and show that $K$ instantiates to $D_\approx$
  \end{itemize}
\end{frame}