# 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.
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**.
