Coding 2023-06-23
I just sketched out the eight basic signatures relevant to group theory. The next thing to look into is the twelve functors that are apparently necessary to represent "forgetting parts of the structure". Most of these should be really easy. (I guess there can be a few more, but, eh.)
After all of that, I can start thinking about functors along the lines of "here is a generator function associated with this structure" and "here are the tests for checking specific properties", and then "here are the tests for checking combinations of properties".
Once I prove that stuff out with simple things like permutation groups, symmetry groups, and modular arithmetic, I can try to build out more elaborate structures, at which point I should have everything I need to work on stuff like geometric algebra.
Just pondering this a little, but I guess the test functors would need something like another set of signatures that just refer to the particular functions in use, and they can use that to be like "whatever module you pass in needs to express these capabilities".
I'm not sure, though. Maybe it's sufficient to say "we compare the behavior to this simpler structure that does test for the property". But where does that leave stuff like commutativity?
I'm going to see if these questions are any less vexing tomorrow.
Good night.