Add constructions for Monads and Comonads

[4e554c4c]

This commit adds a few constructions for monads and comonads. In particular, it adds the identity monad and comonad for a category. It also adds the identity and composite morphism between monads on the same category.

[JacquesCarette]

FYI: might be a few days before I can properly review this. Very welcome additions, I'm just facing a number of deadlines at the moment.

[4e554c4c]

oops sorry for requesting review @Taneb that was on accident

[JacquesCarette]

CI fails with

 Checking Categories.Monad.Strong (/home/runner/work/agda-categories/agda-categories/src/Categories/Monad/Strong.agda).
/home/runner/work/agda-categories/agda-categories/src/Categories/Monad/Strong.agda:47,43-45
Ambiguous name id. It could refer to any one of
  Categories.Monad.id bound at
    /home/runner/work/agda-categories/agda-categories/src/Categories/Monad.agda:35,3-5
  Categories.Monad.Strong.id bound at
    /home/runner/work/agda-categories/agda-categories/src/Categories/Category/Core.agda:23,5-7
id is in scope as
  * a defined name Categories.Monad._.id brought into scope by
    - the opening of Categories.Monad at /home/runner/work/agda-categories/agda-categories/src/Categories/Monad/Strong.agda:19,13-29
    - its definition at /home/runner/work/agda-categories/agda-categories/src/Categories/Monad.agda:35,3-5
  * a record field Categories.Monad.Strong._.id brought into scope by
    - the application of Category at /home/runner/work/agda-categories/agda-categories/src/Categories/Monad/Strong.agda:28,8-16
    - its definition at /home/runner/work/agda-categories/agda-categories/src/Categories/Category/Core.agda:23,5-7
when scope checking id

[4e554c4c]

I ran the CI locally, it seems like everything should pass now