agda / agda-categories

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

F-Coalgebras form a category #354

Closed Taneb closed 1 year ago

Taneb commented 1 year ago

More or less copied from the F-Algebras category. I wanted this while I was messing around with recursion schemes a while back.

t-wissmann commented 1 year ago

Thanks for implementing this -- it also would be useful for me, too!

By the way, there is a space missing in the PR title ('forma' -> 'form a').

JacquesCarette commented 1 year ago

Sorry to be so slow to review this. But now there's a conflict... can you resolve, and then I can merge?

Taneb commented 1 year ago

This was added in #362