\section{Implementation in Agda}

\begin{frame}[t, fragile]{Goals}
  \begin{itemize}
    \item Formalize delay monad (categorically as terminal coalgebra) + properties
    \item Formalize K + properties
    \item Case study on Setoids
  \end{itemize}
\end{frame}

\begin{frame}[t, fragile]{Category theory in Agda}
  agda-categories
\end{frame}

\begin{frame}[t, fragile]{What I managed to show}
  TODO
\end{frame}

\begin{frame}[t, fragile]{Further work}
\begin{itemize}
  \item Show that $\tilde{D}$ is monad (under conditions)
  \item Show that $K \cong \tilde{D}$ (under conditions)
\end{itemize}
\end{frame}