Quiver #262
Quiver #262
Conversation
…sed to be Graphs).
…tion of the category of Graphs. Still a WIP though.
|
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. |
There was a problem hiding this comment.
I wrote this "review" in one go, so it documents my confusion at various points, even if some of it subsequently got resolved. The result is a rather long review, sorry about that. I hope it's helpful in showing where the documentation or module structure could be improved. If not, feel free to ignore the comments that turned out to be addressed somewhere else.
Other than that, most of my comments are about documenting or renaming things.
I didn't spot any technical issues.
There are some more philosophical points too. It still feels like quivers don't quite fit into this library, but I'm not sure how this could be solved or if there's a replacement that would feel more natural. Food for thought.
…oofs from in the category Quivers instance to Data.Quiver.Morphism, where they belong.
…. Make it clear that it goes from StrictCats rather than Cats.
… to its proper places.
…ta.Quiver.Morphism. Add a lot of documentation about the (forced) design choices.
…hsOf. Split some useful bits out of the definition. Some import minimization.
…nt in the name). Make the counit functor more explicit.
|
Ok, everything taken care of! This is much nicer now, thanks. |
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.