leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Update README.md

Browse source
This commit is contained in:
Leon Vatthauer 2023-08-16 13:06:24 +00:00
parent 0764ad31e5
commit 3b93aede06
1 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
README.md
View file

@ -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)