search

agda / agda-categories

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

add kleisli triple #381

Closed Reijix closed 11 months ago

Reijix commented 11 months ago

Small proof that kleisli triples are equivalent to monads. I'm looking for some feedback and then I'd do the same for comonads.

I've defined the kleisli-triple as a typedef for RMonad idF to avoid redundancy, but this might make things a little unclear.

Reijix commented 11 months ago

Thanks for the feedback! I've also added Categories.Comonad.Construction.CoKleisli now.