[ refactor ] Redefine Relation.Binary.Definitions.Adjoint, plus knock-on Function.Consequences#2599
[ refactor ] Redefine Relation.Binary.Definitions.Adjoint, plus knock-on Function.Consequences#2599jamesmckinna wants to merge 15 commits into
Relation.Binary.Definitions.Adjoint, plus knock-on Function.Consequences#2599Conversation
|
I'll return to the merge conflicts after v2.3, given that this is a breaking change. |
|
Given how many of these At present, two existing such items are badly formatted, so at some point, we should fix those up, but I won't try to as part of this PR (though at some level, to me at least, it would 'make sense' to do so, to be consistent with the entry added here... ;-)) |
JacquesCarette
left a comment
There was a problem hiding this comment.
It is easy to remove these links later if we wish, way harder to add them post facto. So I'm all for having them in!
|
Just fixed a typo, and with it the chance to look over everything once again. I'd like to merge this, but at that point, we basically will have duplicate families |
|
I don't understand your comment about duplication? Yes, these are equivalent notions, but with rather different UX, so having them both is definitely a plus. |
|
Thanks @JacquesCarette re:duplication. Will not fiddle any further. |
Fixes #2581 .