Work on slides

slides/bibliography.bib

@@ -1,50 +1,50 @@
+@article{eqlm,
+  title    = {Equational Lifting Monads},
+  journal  = {Electronic Notes in Theoretical Computer Science},
+  volume   = {29},
+  pages    = {22},
+  year     = {1999},
+  note     = {CTCS '99, Conference on Category Theory and Computer Science},
+  issn     = {1571-0661},
+  doi      = {https://doi.org/10.1016/S1571-0661(05)80303-2},
+  url      = {https://www.sciencedirect.com/science/article/pii/S1571066105803032},
+  author   = {Anna Bucalo and Carsten Führmann and Alex Simpson},
+  abstract = {We introduce the notion of an “equational lifting monad” : a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus equational lifting monads precisely capture the (partial) equational properties of partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads.}
+}
+
 @article{moggi,
-author = {Moggi, Eugenio},
+  author     = {Moggi, Eugenio},
-title = {Notions of Computation and Monads},
+  title      = {Notions of Computation and Monads},
-year = {1991},
+  year       = {1991},
-issue_date = {July 1991},
+  issue_date = {July 1991},
-publisher = {Academic Press, Inc.},
+  publisher  = {Academic Press, Inc.},
-address = {USA},
+  address    = {USA},
-volume = {93},
+  volume     = {93},
-number = {1},
+  number     = {1},
-issn = {0890-5401},
+  issn       = {0890-5401},
-url = {https://doi.org/10.1016/0890-5401(91)90052-4},
+  url        = {https://doi.org/10.1016/0890-5401(91)90052-4},
-doi = {10.1016/0890-5401(91)90052-4},
+  doi        = {10.1016/0890-5401(91)90052-4},
-journal = {Inf. Comput.},
+  journal    = {Inf. Comput.},
-month = {jul},
+  month      = {7},
-pages = {55–92},
+  pages      = {55–92},
-numpages = {38}
+  numpages   = {38}
 }
 
 @article{restriction,
-author = {Cockett, J. R. B. and Lack, Stephen},
+  author     = {Cockett, J. R. B. and Lack, Stephen},
-title = {Restriction Categories I: Categories of Partial Maps},
+  title      = {Restriction Categories I: Categories of Partial Maps},
-year = {2002},
+  year       = {2002},
-issue_date = {January},
+  issue_date = {January},
-publisher = {Elsevier Science Publishers Ltd.},
+  publisher  = {Elsevier Science Publishers Ltd.},
-address = {GBR},
+  address    = {GBR},
-volume = {270},
+  volume     = {270},
-number = {1–2},
+  number     = {1–2},
-issn = {0304-3975},
+  issn       = {0304-3975},
-url = {https://doi.org/10.1016/S0304-3975(00)00382-0},
+  url        = {https://doi.org/10.1016/S0304-3975(00)00382-0},
-doi = {10.1016/S0304-3975(00)00382-0},
+  doi        = {10.1016/S0304-3975(00)00382-0},
-abstract = {Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par:Mcat→Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par&r0:Mcat&0 → Ca t0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories and of restriction categories. We also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. A formal system of subobjects is given by a functor into the category sLat of semilattices. This structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an M-category. This M-category contains the universal realization of the given formal subobjects as actual subobjects.},
+  abstract   = {Given a category with a stable system of monics, one can form the corresponding category of partial maps. To each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. This structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. Categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call MCat. The construction of categories of partial maps provides a 2-functor Par:Mcat→Cat. We show that Par can be made into an equivalence of 2-categories between MCat and a 2-category of restriction categories. The underlying ordinary functor Par&r0:Mcat&0 → Ca t0 of the above 2-functor Par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of M-categories and of restriction categories. We also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. A formal system of subobjects is given by a functor into the category sLat of semilattices. This structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an M-category. This M-category contains the universal realization of the given formal subobjects as actual subobjects.},
-journal = {Theor. Comput. Sci.},
+  journal    = {Theor. Comput. Sci.},
-month = {1},
+  month      = {1},
-pages = {223–259},
+  pages      = {223–259},
-numpages = {37}
+  numpages   = {37}
-}
-
-@article{eqlm,
-title = {Equational Lifting Monads},
-journal = {Electronic Notes in Theoretical Computer Science},
-volume = {29},
-pages = {22},
-year = {1999},
-note = {CTCS '99, Conference on Category Theory and Computer Science},
-issn = {1571-0661},
-doi = {https://doi.org/10.1016/S1571-0661(05)80303-2},
-url = {https://www.sciencedirect.com/science/article/pii/S1571066105803032},
-author = {Anna Bucalo and Carsten Führmann and Alex Simpson},
-abstract = {We introduce the notion of an “equational lifting monad” : a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus equational lifting monads precisely capture the (partial) equational properties of partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads.}
 }

slides/main.tex

@@ -160,6 +160,7 @@ Leon Vatthauer%\inst{1}
 \usepackage{tikz}
 \usepackage{tikz-cd}
 \usetikzlibrary{shapes.callouts}
+\usepackage{mathpartir}
 
 \usepackage{xparse}
 

slides/sections/01_abstracting.tex

@@ -4,7 +4,7 @@
 Goal: interpret an effectul programming language in a category $\mathcal{C}$
 
 \begin{itemize}
-  \item<2-> Take a Monad $T$ on $\mathcal{C}$, then values are denoted by objects $A$ and programs by $TA$
+  \item<2-> Take a Monad $T$ on $\mathcal{C}$, then values are denoted by objects $A$ and computations by $TA$
   \item<3-> Programs form a category $\mathcal{C}_T$ with $\mathcal{C}_T(X,Y) := \mathcal{C}(X, TY)$
 \end{itemize}
 
@@ -32,7 +32,7 @@ What properties should a partiality monad $T$ have?
 
 \end{frame}
 
-\newcommand{\tdom}{\text{dom}}
+\newcommand{\tdom}{\text{dom}\;}
 
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Restriction Categories~\cite{restriction}}
 \begin{definition}<1->
@@ -46,15 +46,17 @@ What properties should a partiality monad $T$ have?
   for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow KY, g : X \rightarrow KZ, h: Y \rightarrow KZ$.
 \end{definition}
 
+\onslide<2->
 Intuitively $\tdom f$ captures the domain of definiteness of $f$.
 
-\begin{block}{Remark}<2->
+\begin{block}{Remark}<3->
   Every category has a trivial restriction structure $\tdom f = id$, we call categories with a non-trivial restriction structure \textit{restriction categories}.
 \end{block}
 \end{frame}
 
 \begin{frame}[t, fragile]{Capturing Partiality Categorically}{Equational Lifting Monads~\cite{eqlm}}
   The following criterion is sufficient for guaranteeing that the kleisli category is a restriction category:
+  \pause
   \begin{definition}
     A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
 
@@ -77,9 +79,24 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$.
 % TODO is the maybe monad an equational lifting monad? Ask sergey
 
 \begin{frame}[t, fragile]{The Maybe Monad}
-\begin{itemize}
+\begin{itemize}[<+->]
-  \item Short definition
+  \item $MX = X + 1$
-  \item is equational lifting monad
+  \item on a distributive category 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 \]
+  \item and the following diagram commutes (i.e. it's an equational lifting monad):
+    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0ciJdLFsyLDMsImlkKyEiXSxbMCwzLCJcXGxhbmdsZSBpbmwsaWRcXHJhbmdsZSArICEiLDJdXQ==
+    \[\begin{tikzcd}
+      {X+1} &&& {(X+1)\times(X+1)} \\
+      \\
+      &&& {((X+1)\times X) +((X+1)\times 1)} \\
+      \\
+      &&& {((X+1)\times X)+1}
+      \arrow["\Delta", from=1-1, to=1-4]
+      \arrow["dstr", 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}\]
+  
 \end{itemize}
 \end{frame}
 
@@ -87,13 +104,18 @@ Intuitively $\tdom f$ captures the domain of definiteness of $f$.
 
 \begin{frame}[t, fragile]{The Delay Monad}
 \begin{itemize}
-  \item Definition
+  \item Recall the delay codatatype:
-  \item Strong-Bisimilarity
+    
-  \item Weak-Bisimilarity (Monad?)
+    \[\mprset{fraction={===}}
+    \inferrule {\;} {now\; x : DX}\hskip 2cm
+    \inferrule {c : DX} {later\; c : DX}\]
+
+  \item Categorically: $DX = \nu \gamma. X + \gamma$
+  \item $D$ (if it exists) is a strong and commutative monad (on a cartesian, cocartesian, distributive category)
 \end{itemize}
 \end{frame}
 
-\begin{frame}[t, fragile]{Iteration}
+\begin{frame}[t, fragile]{Partiality from iteration}
 \begin{itemize}
   \item Elgot-Algebras
   \item Free Elgot-Algebras yield monad K