search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
359 stars 67 forks source link

Graded monads #390

Closed sstucki closed 10 months ago

sstucki commented 10 months ago

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 (6e5e05e2934da0bff465906dadc4a6d88dc1a5dc) will become redundant once #389 has been merged.

JacquesCarette commented 10 months ago

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 commented 10 months ago

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: https://github.com/agda/agda-categories/blob/0bd28460c61b0b0317cf599a1b3cc7511ea15534/src/Categories/Monad/Construction/Kleisli.agda#L28

I'm fine with either suggestion, really.

JacquesCarette commented 10 months ago

I prefer GradedKleisliTriple, it is more consistent.

sstucki commented 10 months ago

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

sstucki commented 10 months ago

@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 commented 10 months ago

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