Graded monads

[sstucki]

Apparently, I wrote this a year ago but forgot to submit a PR. It's been sitting on a stale branch in my fork of the repo for a year so it needs to be properly rebased before it's ready to be merged. In particular, the first commit (6e5e05e) will become redundant once #389 has been merged.

[JacquesCarette]

Thanks for GradedMonad, I'm eager to merge that in. I'm not keen on using 'prime' for the name of the alternate definition. Can we try to find a better one? Would KlesliGradedMonad be appropriate?

[sstucki]

I'm not keen on using 'prime' for the name of the alternate definition. Can we try to find a better one? Would KlesliGradedMonad be appropriate?

I agree the current naming isn't great. How about GradedKleisliTriple? That would be consistent with the naming we use for the non-graded case:

agda-categories/src/Categories/Monad/Construction/Kleisli.agda

Line 28 in 0bd2846

KleisliTriple : Set (o ⊔ ℓ ⊔ e)

I'm fine with either suggestion, really.

[JacquesCarette]

I prefer GradedKleisliTriple, it is more consistent.

[sstucki]

I've rebased the old commits on the latest master and fixed the name of the alternate definition to GradedKleisliTriple as agreed, so this is basically ready to be merged now. I'm just waiting on #389 (not sure what the status is there).

[JacquesCarette]

One tiny improvement, and this is ready to go - thanks.

[sstucki]

@JacquesCarette, I fixed Endofuctors.agda as you suggested, although I thought that file would be replaced by #389, once it was ready. I'm not sure what the status of #389 is, the authors haven't replied to the requests for changes, so I'll leave it up to you if you want to wait for that PR to be fixed, or merge the version from this PR instead (that would make #389 obsolete).

[JacquesCarette]

This has waited long enough - I'll merge this in as it is ready.