agda-stdlib Add new module `Effect.Functor.Naperian`

New module Effect.Functor.Naperian added to stdlib. With two records defining Naperian functors:

record RawNaperian
record Naperian.

Jun 22 '23 16:06 Sofia-Insa

I should take this PR over. I'm not entirely sure I know how?

Jan 19 '24 21:01 JacquesCarette

Given the comment of @JacquesCarette above, @jamesmckinna would you be willing to take over this? Otherwise, I'll close it.

Mar 17 '24 12:03 MatthewDaggitt

@MatthewDaggitt @JacquesCarette happy to take over on this one, but it'll be a while before I return proper attention to it, if that's OK?

Mar 17 '24 13:03 jamesmckinna

Minimal cleanup for the time being.

Mar 17 '24 15:03 jamesmckinna

Thanks a lot! I've been wanting to come back to these, but I've barely found enough time to do a few reviews.

Mar 17 '24 15:03 JacquesCarette

This is now back onto my plate to finish. And I even know how to do so!

May 06 '24 01:05 JacquesCarette

This is now back onto my plate to finish. And I even know how to do so!

Fantastic! I'm happy to hand the baton back. But sign me up as a reviewer come the right time...

May 06 '24 07:05 jamesmckinna

The PR is still DRAFT, so I'll revisit/re-review when it's 'ready', but at that point I'll also revisit the early comment above about proving the 'logarithm' properties.

May 07 '24 09:05 jamesmckinna