From 3b93aede063b76697ab867e8682de11a71e6915e Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 16 Aug 2023 13:06:24 +0000 Subject: [PATCH] Update README.md --- README.md | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 4a31592..dff8b9a 100644 --- a/README.md +++ b/README.md @@ -10,12 +10,16 @@ This project uses the awesome category theory library for agda ([agda-categories 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)] +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*) @@ -23,11 +27,19 @@ So far the contributions are: - [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) +- [ ] `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) -- [ ] Refactor `ElgotAlgebras.agda` using `Categories.Morphism.Reasoning` (nicer proofs) +- [X] Refactor `ElgotAlgebras.agda` using `Categories.Morphism.Reasoning` (nicer proofs)