agda-categories
agda-categories copied to clipboard
agda
Various algebraic categories
As illustrative examples and as useful tools in themselves, we can add categories for various algebraic structures. I have an implementation and could turn it into a pull request if it looks good, perhaps as Categories.Category.Instance.Algebraic. Comments and suggestions are most welcome.
If we add these I would like to make sure we also somewhere add that the category of monoids is the same thing as the category of monoid objects in Setoids.
I’ve reworked my definitions of algebraic categories so each is now a one-liner. The key tricks are (a) a more compositional variation on SubCat (needed for _∩_) and (b) generic per-operation homomorphisms (H₀, H₁, H₂ in Homomorphisms). Much tighter than the version I shared previously. An intermediate version shows off map on SubCat, but led to longer definitions than the latest.
I really like to keep lines at 80 columns or narrower, and I didn't succeed this time without harming readability.
The "each is now a one-liner" is absolutely beautiful!
What @Taneb refers to is that I have been reluctant to put too many examples in agda-categories itself. Some examples make sense because they are re-used in category theory itself. So some examples currently live in categories-examples.
Certainly the infrastructure you've developed for doing this is great, and should find a home somewhere standard. Whether it's stdlib or agda-categories, I think it will depend on the piece.
Note that I'm not against putting these examples in agda-categories. There are so succinct, they "show off" something non-trivial about algebraic categories. I just want a bit of discussion first.
… I just want a bit of discussion first.
I’m glad you like them. It’s not clear to me either where these definitions (or further refactorings of them) belong.
Despite considerable effort, I have not yet succeeded in defining the cartesian or cocartesian counterparts to these composable homomorphism building blocks. I ran into trouble with non-injectivity of the U mapping and wasn’t able to sort it out on my own. Still too green with Agda, I guess (in contrast to 25 years of mainly working in Haskell). My stalled attempt is in agda-cat-linear. For now, I’m using a combination of composable and non-composable homomorphisms, which works but isn’t as pretty as I’m after, so I’ve extended only one algebraic category to cartesian, cocartesian, preadditive, and biproduct.
Because the cartesian (etc) SubCat structures need to extend the category SubCat structure, I haven’t found a way to keep the pleasant one-liner definitions that construct and immediately consume SubCats.
If anyone is up for collaborating on extending composable homomorphisms to cartesian and beyond, I’d love the help! It might not take much. I imagine there are some crucial Agda techniques I’ve not yet picked up.
I'm definitely a taker for helping with this. I'm actively working on related ideas, so that wouldn't be a distraction from what I'm doing (which definitely helps with time allocation).
Perhaps that part belongs in issues in your repo?
Many, many months later, I'm finally able to work on this again. Are you still interested @conal ?
Thanks for letting me know, @JacquesCarette. Alas, I had to move on from agda-categories to get unstuck on various issues.
I understand this pragmatic choice.
Nevertheless, I would like to see if it would be possible to have you use agda-categories in the future. I would like to at least make it feasible. So I would like to learn from the obstacles, and what you did in your version to overcome them. I have been able to deal with some of the issues you raised in other tickets.
I’d like to use agda-categories in the future as well! There may be some needed library enhancements, but probably mostly more availability of help when I’m blocked.
My main current project is compositional design of efficient, verified, parallel computation hardware with an elegant denotational basis, structured with category theory. Ideally, all of the category theory (a good chunk of the project) would be from agda-categories. I’m working toward some compelling examples to validate and illustrate the approach. When I have such examples to share, if you’re sufficiently interested and available, we can talk about steps toward replacing my CT code with agda-categories.
Sound good?
Sounds great.
I think my availability will be reasonable this fall term. The winter term might go a little sideways again (very heavy admin load). But I'm hoping to draft others into pitching in. [For more immediate help, the Zulip is usually quite good.]
A suggestion: let’s chat about the denotational hardware project soon, and we’ll see if the goals and approach are sufficiently compelling to you and your collaborators to want to help—as well as what would make it more compelling. The sort of help I’m imagining is mostly advice from the perspectives of category theory and formal proofs, but perhaps the hardware angle will tickle your fancies as well. Then if/when we do start a collaboration, we’ll do so with clear enthusiasm and (at least moderately) realistic expectations.