search

agda / agda-categories

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

Cleanup proofs in Kleisli category construction #378

Closed Taneb closed 1 year ago

Taneb commented 1 year ago

I'm still not quite happy with the proof of assoc′. Open to suggestions there