mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
19 lines
No EOL
561 B
TeX
19 lines
No EOL
561 B
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} |