# BSc Leon Vatthauer

Here I am formalizing some notions of this paper [https://arxiv.org/pdf/2102.11828.pdf](https://arxiv.org/pdf/2102.11828.pdf) in agda.

## 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. Commutative categories [TODO]

## Goals
- [ ] `Monad.Instance.Delay`
    - [X] Formalize the delay monad (as kleisli triple)
    - [ ] Show that a strong delay monad is commutative (also needs formalization of strong delay monad)
- [X] `ElgotAlgebra.agda`
    - [X] Formalize (un-)guarded elgot-algebra.
    - [X] Show the equivalence of `#-Folding` and `#-Compositionality` in the unguarded case. (*Proposition 10*)
- [ ] `ElgotAlgebras.agda`
    - [X] Formalize the category of elgot algebras for a given carrier.
    - [X] Show existence of products in this category
    - [ ] Show existence of exponentials (if carrier has exponentials)
- [ ] `ElgotMonad.agda` [TODO]
    - [ ] Formalize (strong) (pre) elgot monad
    - [ ] Show ElgotMonad->PreElgotMonat
- [ ] Monad K [TODO]
    - [ ] Definitions using free uniform iteration algebras
    - [ ] strength
    - [ ] stable free uniform iteration algebras (and the relation to CCC carriers)
- [ ] ...
- [ ] Theorem 37 [TODO] (final goal)

## Roadmap
TODO

## TODOs
- [ ] Create Roadmap (find what theorem 37 depends on and then create a game plan)
- [X] Refactor `ElgotAlgebras.agda` using `Categories.Morphism.Reasoning` (nicer proofs)