Category of endofunctors is monoidal

agda / agda-categories

A new Categories library for Agda

https://agda.github.io/agda-categories

MIT License

359 stars 67 forks source link

Category of endofunctors is monoidal #389

Closed iwilare closed 10 months ago

iwilare commented 10 months ago

We couldn't find an instance of Monoidal for the category of endofunctors [C,C] for a category C, so we wrote one!

JacquesCarette commented 10 months ago

Note that there will be a harder merge needed because of #390.

iwilare commented 10 months ago

Sorry for the late reply, thank you for the useful suggestion! We never stop learning all the various idiosyncracies that make a good Agda PR. I think #390 makes our contribution obsolete, right? The version suggested in #390 looks way better than ours, I'm okay with just keeping that and closing this one!