slides are in a somewhat final state

slides/bibliography.bib

@@ -35,7 +35,9 @@
   number    = {2},
   journal   = {Mathematical Structures in Computer Science},
   publisher = {Cambridge University Press},
-  author    = {ADÁMEK, JIŘÍ and MILIUS, STEFAN and VELEBIL, JIŘÍ},
+  author    = {Jir{\'{\i}} Ad{\'{a}}mek and
+               Stefan Milius and
+               Jir{\'{\i}} Velebil},
   year      = {2011},
   pages     = {417–480}
 }

slides/main.tex

@@ -7,7 +7,7 @@
 % of the GNU Public License, version 2.
 %
 % ------------------------------------------------------------------------------
-\documentclass[final, handout]{beamer}
+\documentclass[final]{beamer}
 
 % ========================================================================================
 % Theme: inner, outer, font and colors
@@ -46,7 +46,7 @@
 % custom commands for symbols
 \usepackage{styles/symbols}
 
-
+\newcommand*\quot[2]{{^{\textstyle #1}\big/_{\textstyle #2}}}
 % ========================================================================================
 % Setup for Titlepage
 % ----------------------------------------------------------------------------------------
@@ -87,7 +87,7 @@ Leon Vatthauer%\inst{1}
 			sortcites=true,% sort citations when multiple entries are passed to one cite command
 			doi=true,%
 			isbn=false,%
-			url=false,%
+			% url=false,%
 			eprint=false,%
 			backend=biber%
 		   ]{biblatex}
@@ -195,7 +195,7 @@ at (#3) {#4};
 	\input{sections/02_goals.tex}
 
 	% bibliography
-	\begin{frame}[t]{Bibliography}
+	\begin{frame}[allowframebreaks]{Bibliography}
 		\printbibliography[heading=none]
 	\end{frame}
 

slides/sections/01_abstracting.tex

@@ -36,7 +36,7 @@ What properties should a monad $T$ for modelling partiality have?
 
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Preliminaries}
   We work in category $\mathcal{C}$ that
-  \begin{itemize}
+  \begin{itemize}[<+->]
     \item has finite products
     \item has finite coproducts
     \item is distributive, i.e. the following is an iso:
@@ -50,6 +50,7 @@ What properties should a monad $T$ for modelling partiality have?
       {X \times (Y + Z)} &&&& {(X \times Y) + (X \times Z)}
       \arrow["dstl", from=1-1, to=1-5]
     \end{tikzcd}\]
+    \item has a natural numbers object $\mathbb{N}$ (which is stable)
   \end{itemize}
   
 \end{frame}
@@ -65,7 +66,7 @@ What properties should a monad $T$ for modelling partiality have?
     \tdom(g \circ (\tdom f)) &= (\tdom g) \circ (\tdom f)\\
     (\tdom h) \circ f &= f \circ \tdom (h \circ f)
   \end{alignat}
-  for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow KY, g : X \rightarrow KZ, h: Y \rightarrow KZ$.
+  for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
 \end{definition}
 
 \onslide<2->
@@ -104,8 +105,8 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{The Maybe Monad}
 \begin{itemize}[<+->]
   \item $MX = X + 1$
-  \item on a distributive category the maybe monad is strong and commutative:
+  \item The maybe monad is strong and commutative:
-    \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstr}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+1}{\longrightarrow} (X \times Y) + 1 \]
+    \[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1 \]
   \item and the following diagram commutes (i.e. it is an equational lifting monad):
     % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0ciJdLFsyLDMsImlkKyEiXSxbMCwzLCJcXGxhbmdsZSBpbmwsaWRcXHJhbmdsZSArICEiLDJdXQ==
     \[\begin{tikzcd}
@@ -115,7 +116,7 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
       \\
       &&& {((X+1)\times X)+1}
       \arrow["\Delta", from=1-1, to=1-4]
-      \arrow["dstr", from=1-4, to=3-4]
+      \arrow["dstl", from=1-4, to=3-4]
       \arrow["{id+!}", from=3-4, to=5-4]
       \arrow["{\langle inl,id\rangle + !}"', from=1-1, to=5-4]
     \end{tikzcd}\]
@@ -131,13 +132,13 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
     \inferrule {x : X} {now\; x : DX}\hskip 2cm
     \inferrule {c : DX} {later\; c : DX}\]
 
-  \item Categorically: $DX = \nu A. X + A$
+  \item $DX = \nu A. X + A$
   \item By Lambek we get $DX \cong X + DX$ which yields:
   \begin{alignat*}{2}
     &out &&: DX \rightarrow X + DX\\
     &out^{-1} &&: X + DX \rightarrow DX = [ now , later ]
   \end{alignat*}
-  \item $D$ (if it exists) is a strong and commutative monad (on a cartesian, cocartesian, distributive category)
+  \item $D$ (if it exists) is a strong and commutative monad
   \item $D$ is not an equational lifting monad, because besides modelling partiality, it also counts steps \\(e.g. $now\; c \not= later\; (now\; c)$)
 \end{itemize}
 \end{frame}
@@ -146,25 +147,34 @@ Intuitively $\tdom f$ captures the domain of definedness of $f$.
 % \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={===}}
+  \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm
+  \inferrule {p \approx q} {later\; p \approx later\; q}\]
+  \pause
+  where
+  \[
+  \inferrule {\;} {now\;c \downarrow c}\hskip 2cm
+  \inferrule {x \downarrow c} {later\; x \downarrow c}\]
+  \pause
+  we can model this as the coequalizer:
+  % https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFhcXHRpbWVzIFxcbWF0aGJie059KSJdLFsyLDAsIkRYIl0sWzQsMCwiRF9cXGFwcHJveCJdLFswLDEsIlxcaW90YV4qIiwwLHsib2Zmc2V0IjotMn1dLFswLDEsIkQgZnN0IiwyLHsib2Zmc2V0IjoyfV0sWzEsMiwiXFxyaG9fWCJdXQ==
+  \[\begin{tikzcd}
+    {D(X\times \mathbb{N})} && DX && {D_\approx X}
+    \arrow["{\iota^*}", shift left=2, from=1-1, to=1-3]
+    \arrow["{D fst}"', shift right=2, from=1-1, to=1-3]
+    \arrow["{\rho_X}", from=1-3, to=1-5]
+  \end{tikzcd}\]
+  \pause
+  \textbf{Problem}: Defining $\mu_X : D_\approx^2 X \rightarrow D_\approx X$ requires countable choice.
+\end{frame}
 
-
+\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras}
-%%%%%%%%
+\pause
-% NOTE:
+The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}~\cite{elgotalgebras}:
-% quotienting D should be covered later in the agda chapter, not here!
-
-% \begin{frame}[t, fragile]{The quotiented Delay Monad}
-%   Following the work in~\cite{quotienting} we quotient $D$ by weak bisimilarity: 
-%   \[\mprset{fraction={===}}
-%   \inferrule {p \downarrow c \\ q \downarrow c} {p \approx q}\hskip 2cm
-%   \inferrule {p \approx q} {later\; p \approx later\; q}\]
-
-% \end{frame}
-%%%%%%%
-
-\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Algebras~\cite{elgotalgebras}}
-The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complete Elgot Algebras}:
 \begin{definition}
-  A (unguarded) Elgot Algebra consists of:
+  A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
   \begin{itemize}
     \item An object X
     \item for every $f : S \rightarrow X + S$ the iteration $f^\# : S \rightarrow X$, satisfying:
@@ -184,16 +194,20 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet
 \end{frame}
 
 \begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}}
-Recall the following notion:
 \begin{definition}
   A monad $\mathbf{T}$ is an Elgot monad if it has an iteration operator $(f : X \rightarrow T(Y + X))^\dagger : X \rightarrow TY$ satisfying:
   \begin{itemize}
-    \item \textbf{Fixpoint}:
+    \item \textbf{Fixpoint}: $f^\dagger = [ \eta , f^\dagger ]^* \circ f$
-    \item \textbf{Naturality}:
+    \\for $f : X \rightarrow T(Y + X)$
-    \item \textbf{Codiagonal}:
+    \item \textbf{Uniformity}: $f \circ h = T(id + h) \circ g \Rightarrow f^\dagger \circ h = g^\dagger$
-    \item \textbf{Uniformity}:
+    \\for $f : X \rightarrow T(Y + X) , g : Z \rightarrow T(Y + Z)$
+    \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$
+    \\for $f : X \rightarrow T((Y + X) + X)$
   \end{itemize}
 \end{definition}
+\pause
 \begin{block}{Remark}
 Strong Elgot Monads are regarded as minimal semantic structures for interpreting effectful while-languages.
 \end{block}
@@ -209,6 +223,7 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
     A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that Kleisli lifting is iteration preversing, i.e.
     \[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
   \end{definition}
+  \pause
   \begin{theorem}
     Every Elgot monad is pre-Elgot
   \end{theorem}
@@ -216,15 +231,33 @@ Strong Elgot Monads are regarded as minimal semantic structures for interpreting
 
 \begin{frame}[t, fragile]{Partiality from iteration}{The initial pre-Elgot Monad~\cite{uniformelgot}}
   \begin{itemize}[<+->]
-    \item By defining $KX$ as the free Elgot algebra over $X$ we get a monad $K$
+    \item By defining $KX$ as the free Elgot algebra over $X$ we get a monad $K$ (that we assume is stable)
     \item $K$ is strong and commutative
     \item $K$ is an equational lifting monad
     \item $K$ is the initial pre-Elgot monad
   \end{itemize}
 \end{frame}
 
-\begin{frame}[t, fragile]{Partiality from iteration}{Closing the gap}
+\begin{frame}[t, fragile]{Partiality from iteration}{Closing the gap~\cite{uniformelgot}}
-  ...
+  Let's look at $\mathbf{K}$ under various assumptions:
+  \begin{itemize}[<+->]
+    \item \textbf{Assuming excluded middle:}
+    
+    \begin{itemize}[<+->]
+      \item The initial pre-Elgot monad and the initial Elgot monad coincide
+      \item $DX \cong X \times \mathbb{N} + 1$
+      \item $D_\approx X \cong X + 1$
+      \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
+      \item $D_\approx$ is the initial (pre-)Elgot Monad ($\Rightarrow K \cong D_\approx$).
+    \end{itemize}
+    
+  \end{itemize}
 \end{frame}
 
 

slides/sections/02_goals.tex

@@ -1,7 +1,7 @@
 \section{Implementation in Agda}
 
 \begin{frame}[t, fragile]{Goals}
-  \begin{itemize}
+  \begin{itemize}[<+->]
     \item Formalize the delay monad categorically and show that it is..
     \begin{itemize}
       \item strong
@@ -13,15 +13,27 @@
       \item commutative
       \item an equational lifting monad
     \end{itemize}
-    \item Take the category of setoids and show that $K$ instantiates to $D$ quotiented by weak-bisimilarity
+    \item Take the category of setoids and show that $K$ instantiates to $D_\approx$
   \end{itemize}
 \end{frame}
 
-\begin{frame}[t, fragile]{Category theory in Agda}
+\begin{frame}[t, fragile, blank]{Category Theory in Agda}{Setoid-enriched Categories}
-  agda-categories
+  \begin{minted}{agda}
-\end{frame}
+record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
+  field
+    Obj : Set o
+    _⇒_ : Obj → Obj → Set ℓ
+    _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e
 
-\begin{frame}[t, fragile]{Resumee}
+    id  : ∀ {A} → (A ⇒ A)
-  On doing category theory in agda
+    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
-  (pro/con)
+
+  field
+    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} 
+      → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
+    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
+    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
+    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
+    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
+  \end{minted}
 \end{frame}