🎨 rewrite index

.gitattributes

@@ -1 +1,2 @@
-*.lagda.md linguist-detectable=true
+*.lagda.md linguist-language=Literate Agda
+*.lagda.md linguist-detectable=true

.gitignore

@@ -1,7 +1,7 @@
 *.agdai
 *.pdf
 *.log
-Everything.agda
+src/Everything.agda
 public/
 .direnv
 .DS_Store

Makefile

@@ -14,7 +14,7 @@ agda: Everything.agda
 	cp Agda.css public/Agda.css
 
 clean:
-	rm -f  Everything.agda
+	rm -f src/Everything.agda
 	rm -rf public/*
 	find . -name '*.agdai' -exec rm \{\} \;
 
@@ -29,7 +29,7 @@ push':
 	mv bsc-thesis public
 
 Everything.agda:
-	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda
+	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > src/Everything.agda
 
 open:
 	firefox public/index.html

src/index.lagda.md

@@ -6,12 +6,22 @@ To see a full list of all the modules go to:
 open import Everything
 ```
 
-For my bachelor's thesis I am implementing categorical notions of partiality in agda using the *agda-categories* library. The repo for this project can be found [here](https://git8.cs.fau.de/theses/bsc-leon-vatthauer).
-This mostly is an implementation of this paper by Sergey Goncharov: [arxiv](https://arxiv.org/abs/2102.11828)
+For my bachelor thesis I am implementing categorical notions of partiality in agda using the *agda-categories* library. The repo for this project can be found [here](https://git8.cs.fau.de/theses/bsc-leon-vatthauer).
+This is an implementation of this paper by Sergey Goncharov: [arxiv](https://arxiv.org/abs/2102.11828)
 
-## Structure
+## Index
 
-We start out by formalizing Caprettas Delay Monad in category theory by existence of final coalgebras and showing that it is strong.
+### Preliminaries
+
+The work takes place in an ambient category that fits our needs:
+
+```agda
+open import Category.Instance.AmbientCategory
+```
+
+### Delay Monad
+
+We start out by formalizing Capretta's *Delay Monad* in a categorical setting and then proving that it is strong and commutative.
 
 ```agda
 open import Monad.Instance.Delay
@@ -19,37 +29,60 @@ open import Monad.Instance.Delay.Strong
 open import Monad.Instance.Delay.Commutative
 ```
 
-The next step is to quotient the delay monad by weak bisimilarity, in category theory this corresponds to existence of fitting coequalizers.
-This quotiented structure is not directly monadic, we implement conditions under which it extends to a monad and prove it.
+The next step is to quotient the delay monad by weak bisimilarity, but this quotiented structure is not monadic, so we postulate conditions under which it extends to a monad.
 
 ```agda
 open import Monad.Instance.Delay.Quotienting
 ```
 
-Next come some basic definitions of iteration algebras, we differentiate between uniform-iteration algebras and (un-)guarded elgot algebras:
+### Monad K
+
+The goal of this last section is to formalize an equational lifting monad **K** that generalizes both the maybe monad and the delay monad.
+
+To do so we first need to look at iteration structures, i.e. functor algebras with an iteration operator.
+We differentiate between two kinds of iteration structures, *Elgot algebras* and *uniform-iteration algebras* where the latter is less restrictive than the former.
 
 ```agda
 open import Algebra.ElgotAlgebra
-open import Category.Construction.ElgotAlgebras
 open import Algebra.UniformIterationAlgebra
+```
+
+Afterwards we also introduce categories of iteration algebras with iteration preserving morphisms:
+
+```agda
+open import Category.Construction.ElgotAlgebras
 open import Category.Construction.UniformIterationAlgebras
 ```
 
-Existence of free uniform-iteration algebras yields a monad that is of interest to us, we call it **K** and want to show some of it's properties (i.e. that it is strong and an equational lifting monad):
+Lastly we need a notion of *stability* for uniform-iteration algebras:
+
+```agda
+open import Algebra.Properties
+```
+
+With this in hand we can now define *KX* as a *free uniform-iteration algebra* and proof that under *stability* it is a strong monad.
 
 ```agda
 open import Monad.Instance.K
 open import Monad.Instance.K.Strong
 ```
 
-Later we will also show that free uniform-iteration algebras coincide with free elgot algebras
+The next step is to show that every *KX* satisfies compositionality, meaning that each *KX* is an Elgot algebra.
 
 ```agda
--- TODO
+open import Monad.Instance.K.Compositionality
 ```
 
-For the final step we will come back to the quotiented delay monad and show that under variations of the axiom of countable choice it is an explicit construction for the aforementioned monad **K**.
+and with this we can show that K is and equational lifting monad, i.e. a commutative monad satisfying the equational lifting law:
 
 ```agda
-open import Monad.Instance.Delay.Properties
+open import Monad.Instance.K.Commutative
+open import Monad.Instance.K.EquationalLifting
+```
+
+and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is pre-Elgot.
+
+```agda
+open import Monad.ElgotMonad
+-- open import Monad.Instance.K.PreElgot TODO
 ```