def: 1-category Monad(C)

[favonia]

Description

Define the 1-category of monads.

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

[Lavenza]

Pull request preview

[favonia]

This is my first serious 1lab contribution and I probably messed up things. 😅

[ncfavier]

Looks pretty good!

[favonia]

@ncfavier Question: should I write "id", "Id", or "1" for identity functors and identity natural transformations? I checked a few more pages and found that it's not entirely consistent. 🤔

[ncfavier]

"Id" is fine for functors, and "id" for natural transformations