✨ Added index with some nice text

Makefile

@@ -9,10 +9,9 @@ pandoc: public/*.md
 	)
 
 agda: Everything.agda
-	agda --html --html-dir=public Everything.agda --html-highlight=auto -i.
+	agda --html --html-dir=public index.lagda.md --html-highlight=auto -i.
 	rm -f public/Agda.css
 	cp Agda.css public/Agda.css
-	mv public/Everything.html public/index.html
 
 clean:
 	rm -f  Everything.agda

index.lagda.md

@@ -0,0 +1,52 @@
+# Implementing Categorical Notions of Partiality and Delay in Agda
+
+To see a full list of all the modules go to:
+
+```agda
+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)
+
+## Structure
+
+We start out by formalizing Caprettas Delay Monad in category theory by existence of final coalgebras and showing that it is strong.
+
+```agda
+open import Monad.Instance.Delay
+```
+
+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.
+
+```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:
+
+```agda
+open import Algebra.ElgotAlgebra
+open import Category.Construction.ElgotAlgebras
+open import Algebra.UniformIterationAlgebra
+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):
+
+```agda
+open import Monad.Instance.K -- TODO move to Monad.Construction.K
+```
+
+Later we will also show that free uniform-iteration algebras coincide with free elgot algebras
+
+```agda
+-- TODO
+```
+
+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**.
+
+```agda
+open import Monad.Instance.Delay.Properties
+```

src/Monad/Instance/Delay/Properties.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Functor
 open import Category.Instance.AmbientCategory using (Ambient)

src/Monad/Instance/K.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.FreeObjects.Free
 open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)