JacquesCarette
commented
3 years ago Note that one of the things I'm considering is submitting Quiver (and some other pieces) to stdlib, and maybe move a certain amount of the categorical stuff to categories-examples, as this stuff really doesn't need to be in agda-categories per se.
This is a rather large refactor of what used to be Graph into Quiver (as that's really the more appropriate name for this context). It's not necessarily fully done, but I want feedback before I continue.