diff --git a/README.md b/README.md
index dd3e574..4a31592 100644
--- a/README.md
+++ b/README.md
@@ -5,8 +5,29 @@ Here I am formalizing some notions of this paper [https://arxiv.org/pdf/2102.118
 ## 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) [[**WIP**](https://github.com/agda/agda-categories/pull/383)]
+    - `Categories.Category.Distributive`
+    - `Categories.Category.Extensive.Bundle`
+    - `Categories.Category.Extensive.Properties.Distributive`
+
 ## Goals
-TODO
+- [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)
+- [ ] Theorem 37 (final goal)
 
 ## Roadmap
-TODO
\ No newline at end of file
+TODO
+
+## TODOs
+- [ ] Create Roadmap (find what theorem 37 depends on and then create a game plan)
+- [ ] Refactor `ElgotAlgebras.agda` using `Categories.Morphism.Reasoning` (nicer proofs)