Update README.md

README.md

@@ -4,27 +4,6 @@ Here I am formalizing some notions of this paper [https://arxiv.org/pdf/2102.118
 The whole project consists of literate agda files, where I add my documentation as markdown.
 A (mostly up to date) version can be found here: https://wwwcip.cs.fau.de/~hy84coky/bsc-thesis/
 
-## Running the project
-TODO
-
-## Contributions to *agda-categories*
-This project uses the awesome category theory library for agda ([agda-categories](https://github.com/agda/agda-categories)), it is already very extensive, but some notions needed here are missing, so I contribute them to the library.
-So far the contributions are:
-1. Kleisli triples [[merged](https://github.com/agda/agda-categories/pull/381)]
-    - `Categories.Monad.Construction.Kleisli`
-2. Distributive categories (and the relation to extensivity) [[merged](https://github.com/agda/agda-categories/pull/383)]
-    - `Categories.Category.Distributive`
-    - `Categories.Category.Extensive.Bundle`
-    - `Categories.Category.Extensive.Properties.Distributive`
-3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
-    - `Categories.Object.NaturalNumbers.Parametrized`
-    - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
-    - `Categories.Object.NaturalNumbers.Properties.Parametrized`
-4. Commutative monad [TODO]
-
-## TODO
-TODOs are found inside the literate agda files!
-
 ## Usage
 The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
 
@@ -39,3 +18,20 @@ There is also a Makefile for compiling every module and generating the html docu
 ```
 make
 ```
+
+## Contributions to *agda-categories*
+This project uses the awesome category theory library for agda ([agda-categories](https://github.com/agda/agda-categories)), it is already very extensive, but some notions needed here are missing, so I contribute them to the library.
+So far the contributions are:
+1. Kleisli triples [[merged](https://github.com/agda/agda-categories/pull/381)]
+    - `Categories.Monad.Construction.Kleisli`
+2. Distributive categories (and the relation to extensivity) [[merged](https://github.com/agda/agda-categories/pull/383)]
+    - `Categories.Category.Distributive`
+    - `Categories.Category.Extensive.Bundle`
+    - `Categories.Category.Extensive.Properties.Distributive`
+3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
+    - `Categories.Object.NaturalNumbers.Parametrized`
+    - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
+    - `Categories.Object.NaturalNumbers.Properties.Parametrized`
+4. Commutative monad [[merged](https://github.com/agda/agda-categories/pull/404)]
+    - `Categories.Monad.Commutative`
+    - `Categories.Monad.Strong.Properties`

slides/bibliography.bib

@@ -127,3 +127,19 @@ numpages = {16}
   biburl     = {https://dblp.org/rec/journals/corr/abs-2102-11828.bib},
   bibsource  = {dblp computer science bibliography, https://dblp.org}
 }
+
+@article{while,
+  author     = {Sergey Goncharov and
+                Lutz Schr{\"{o}}der and
+                Christoph Rauch},
+  title      = {(Co-)Algebraic Foundations for Effect Handling and Iteration},
+  journal    = {CoRR},
+  volume     = {abs/1405.0854},
+  year       = {2014},
+  url        = {http://arxiv.org/abs/1405.0854},
+  eprinttype = {arXiv},
+  eprint     = {1405.0854},
+  timestamp  = {Mon, 13 Aug 2018 16:47:19 +0200},
+  biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
+  bibsource  = {dblp computer science bibliography, https://dblp.org}
+}

slides/code-examples/reverse.agda

@@ -29,8 +29,8 @@ module reverse where
   fin-colist : Colist ℕ
   fin-colist = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ []))
 
-  inf-colist : Colist ℕ
-  inf-colist = 1 ∷ ♯ inf-colist
+  ones : Colist ℕ
+  ones = 1 ∷ ♯ ones
 
   -- run reverse fin-colist for 5 steps
-  -- run reverse inf-colist for 1000 steps
+  -- run reverse ones for 1000 steps

slides/sections/01_abstracting.tex

@@ -170,7 +170,7 @@ The following is an adaptation of Ad\'amek, Milius and Velebil's \textit{complet
 \end{block}
 \end{frame}
 
-\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}}
+\begin{frame}[t, fragile]{Partiality from Iteration}{Elgot Monads~\cite{elgotmonad}~\cite{while}}
 \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}