minor fix

slides/code-examples/reverse.agda

@@ -1,5 +1,4 @@
 {-# OPTIONS --guardedness #-}
--- open import Codata.Musical.Colist hiding (_++_)
 open import Codata.Musical.Notation
 open import Data.Nat
 open import Data.Nat.Show renaming (show to showℕ)

slides/sections/00_intro.tex

@@ -55,13 +55,18 @@
     \end{minted}
   \end{multicols}
 
-  \item What about \mintinline{agda}|reverse|?
+  \item What about \mintinline{agda}|reverse| for (possibly) infinite lists:
+  \begin{minted}{agda}
+    data Colist (A : Set) : Set where
+      [] : Colist A
+      _∷_ : A → ∞ (Colist A) → Colist A
+  \end{minted}
   
 \end{itemize}
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality in Agda}{Capretta's Delay Monad}
-  \begin{itemize}
+  \begin{itemize}[<+->]
     \item Capretta's Delay Monad is a \textbf{coinductive} data type whose inhabitants can be viewed as suspended computations. 
     \vskip 0.5cm
     \begin{minted}{agda}
@@ -92,13 +97,6 @@
 
 \begin{itemize}
   \item Now we can define a reverse function for possibly infinite lists:
-  \vskip 0.5cm
-  \begin{minted}{agda}
-    data Colist (A : Set) : Set where
-      [] : Colist A
-      _∷_ : A → ∞ (Colist A) → Colist A
-  \end{minted}
-  \vskip 0.5cm
   \begin{minted}{agda}
     reverse : ∀ {A : Set} → Colist A → Delay (Colist A)
     reverse {A} = revAcc []

slides/sections/01_abstracting.tex

@@ -13,21 +13,6 @@ What properties should a monad $T$ for modelling partiality have?
 
 \begin{enumerate}
   \item<5-> Commutativity (also entails strength)
-  % , i.e. the following programs should yield equal results:
-  %   \begin{multicols}{2}
-  %     \begin{minted}{haskell}
-  %       do x <- p
-  %          y <- q
-  %          return (x, y)
-  %       \end{minted}
-        
-  %       \begin{minted}{haskell}
-  %       do y <- q
-  %          x <- p
-  %          return (x, y)
-  %     \end{minted}
-  %   \end{multicols}
-  %   where p and q are programs.  
   \item<6-> Morphisms in $\mathcal{C}_T$ should be partial maps
   \item<7-> There should be no other effect besides partiality
 \end{enumerate}
@@ -99,9 +84,6 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
   \end{theorem}
 \end{frame}
 
-% write on board:
-% equational lifting: do x <- p; return (return x, x) = do x <- p; return (p, x)
-
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{The Maybe Monad}
 \begin{itemize}[<+->]
   \item $MX = X + 1$
@@ -143,10 +125,6 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
 \end{itemize}
 \end{frame}
 
-% write on board:
-% \eta = now
-% given f : X \rightarrow TY, f* is defined by corecursion.
-
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Quotienting the Delay Monad~\cite{quotienting}}
   Following the work by Chapman, Uustalu and Veltri we can quotient $D$ by the 'correct' kind of equality:
   \[\mprset{fraction={===}}
@@ -171,7 +149,6 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras}
-\pause
 The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}~\cite{elgotalgebras}:
 \begin{definition}
   A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
@@ -200,7 +177,7 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet
     \item \textbf{Fixpoint}: $f^\dagger = [ \eta , f^\dagger ]^* \circ f$
     \\for $f : X \rightarrow T(Y + X)$
     \item \textbf{Uniformity}: $f \circ h = T(id + h) \circ g \Rightarrow f^\dagger \circ h = g^\dagger$
-    \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z)$
+    \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z), h : Z \rightarrow X$
     \item \textbf{Naturality}: $g^* \circ f^\dagger = ([ (T inl) \circ g , \eta \circ inr ]^* \circ f )^\dagger$
     \\for $f : X \rightarrow T(Y + X), g : Y \rightarrow TZ$
     \item \textbf{Codiagonal}: $f^{\dagger\dagger} = (T[id , inr ] \circ f)^\dagger$
@@ -214,9 +191,6 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
 
 \end{frame}
 
-
-% TODO 
-% maybe dont talk about elgot monads at all, give intuition for the initial pre Elgot monad.
 \begin{frame}[t, fragile]{Partiality from Iteration}{pre-Elgot Monads~\cite{uniformelgot}}
   Relaxing the requirements for Elgot monads we get the following weaker concept:
   \begin{definition}
@@ -250,7 +224,6 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
       \item $X + 1$ is the initial (pre-)Elgot monad ($\Rightarrow K \cong (-)+1 \cong D_\approx$)
     \end{itemize}
     
-    % \\$\Rightarrow$ $X+1$ is the initial pre-Elgot Monad and also the initial Elgot Monad.
     \item \textbf{Assuming countable choice:}
     \begin{itemize}[<+->]
       \item The initial pre-Elgot monad and the initial Elgot monad coincide
@@ -258,9 +231,4 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
     \end{itemize}
     
   \end{itemize}
-\end{frame}
+\end{frame}
-
-
-%% TODOs:
-% cite stefan
-% cite sergey