opposite of a Ring
#1900
opposite of a Ring
#1900
Conversation
There was a problem hiding this comment.
Nice.
But also: the infamous 'Op' meta-functor. Claudio Sacerdoti Coen and I spent two full afternoons in front a blackboard working out the details of what it actually means. And how it ought to be automated. We never got around to writing anything up, unfortunately.
|
Well, re not-written-up work: I'd love to see notes (or rational reconstruction) of that discussion with Claudio, but I suppose I was wanting to... for once ;-)... not get too caught up with the 'in full generality' situation, in the spirit of your previous comments about writing 'smaller' PRs... |
|
And: should such an 'Op' reverse the equivalence relation? I had considered this, with a view (de-strictifying, bicategories vs. 2-categories etc.) to having Op on Setoids being an iso, not a definitional equality... but not today... |
|
Looked for my notes, and didn't find them in the notebooks where I expected them to be. Sigh. Ah, but I do have pictures of the boards! So whether 'Op' should reverse the equivalence relation indeed is mixed up with whether you're looking at things 1- or 2-categorically. Of course, 2-categorically, there are 3 choices of what to flip, so that there should be 3 'flip' operations. |
src/Algebra/Construct/Flip/Op.agda
Outdated
|
|
||
| module _ (+ : Op₂ A) where | ||
|
|
||
| distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + |
There was a problem hiding this comment.
The other thing we could do to make this is a little nicer is to import Algebra.Definitions and Algebra.Structures locally in each anonymous module parameterised by the equality. Which would then allow us to avoid messing up the infix notation here?
There was a problem hiding this comment.
Ah... will now turn to this.
And it seems that this applies throughout, even to the original module contents: so I've now named each previously anonymous module, and opened it locally in place with the appropriate arguments. is this better now? See most recent commit.
Or 8 operations? For |
|
I won't comment on the multiplicities of |
|
Isn't the 4th possibility 'do nothing', which is why it's hard to see it? We're talking about a group with 4 elements, which is the product of the group with 2 elements, so it's rather natural that only 3 of them show up! |
|
D'oh! |
Revert "added `CommutativeRing` to the tally" This reverts commit 5baffde.
|
Oh man, it's too late in the evening to be doing this. I've let yet more bogus commits enter the PR. 🤦 And it clearly goes back to before the most recent commit/revert. @#$% |
… branch/PR Revert "`CHANGELOG`" This reverts commit e54f2a7.
|
OK, I've screwed this one up as well. Converting to draft and then sitting on my hands for a few days. |
|
Nope... those reversions didn't work either. It looks as though this one was broken from the start. Try again another day with a fresh pr. |
Haha yes. Whoops, sorry for throwing out that confusing statement 😅 |
|
To follow up on my comments form a week ago (or more). I'll start a fresh branch and roll up the commits form this one, and then open a fresh PR. So this one moved to 'Draft' while I thought about it some more, and of course lots has changed in the meantime, but this one should be a very 'local' change. |
jamesmckinna
added
the
status: duplicate
|
superseded by #1910 |
…)" This reverts commit 7772dee.
This reverts commit 7772dee.
This reverts commit 7772dee.
See discussion in issue #1888 and associated pr #1898
EDITED
See also the discussion of issue #1617 and associated PR #1684: some slight crunchiness arises from the decision to make
IsRingetc. properties on top of+-AbelianGroup, rather than two structures over a shared commonSetoidsubstructure.TODOs:
IsRing,Ring: not for any of the intermediate structures/bundles