Jacques Carette
Jacques Carette
I think that introducing these concepts is a good idea. What's the definition of `Inverseʳ` now? (Making these issues more self-contained would be good -- we don't have millions of...
If we had "comments as valid code" like was discussed earlier today, then your `HalfRightAdjoint` definition could become checkable-comments. Maybe that's the better route forward? Another might be to embrace...
That seems reasonable.
Might be best to not worry about `Semiring` for now? Perfect is the enemy of progress or some such.
I prefer this one.
Is it spelled out somewhere what the `Semiring`-action refactoring is that is blocking work on here?
The data, at the time, didn't support my 'hunch' that `∙-cong` was the better way to go. Really, `cong` for an n-ary operator should take that operator *symbol* as input,...
Right - I did want to abstractly discuss `hypothetical-rewrite`, and agree that the current best solution is to embed the name of the operation in the name, consistently.
Ghastly. But such is the fate of the functional representation. So much right-programming, just when I'd gotten used to the beauty of left-programming! I wish there were a better symbol...