Add new `Bool` action on a `RawMonoid` plus properties

[jamesmckinna]

Prompted by @JacquesCarette 's desire to further systematise the refactoring in #2407 , this adds two operations which appear ad hoc in the normal form semantics for IdempotentCommutativeMonoids, but are yet more instances of a (Raw)MonoidAction cf. #2348 / #2350 by analogy with the corresponding actions in the normal form semantics for CommutativeMonoids.

NB

• Nat-action arises because (Nat, +, 0) is the free commutative monoid on one generator...
• similarly, (Bool, /, true) is, I think, the free idempotent commutative monoid on one generator?

Could be left as DRAFT, pending further work cf. #2351 , but worth inviting review now, I think.

NB. possible issues:

• names of things: current notation is terrible, unfortunately, so suggestions welcome!
• left-/right- symmetric versions, ie. x + n × y as well as n × x + y etc.
• possible refactoring of the existing definitions as instances of these generalised 'affine' ones?
• refactoring not yet applied to Algebra.Solver.*Monoid etc.
• ... further systematisation of existing Algebra.Definitions.RawMonoid._×_ operation etc. possible as well?
• Fairbairn threshhold?

[jamesmckinna]

Ooops (mistake to try to abstract immediately over MonoidAction... the Nat case is a MagmaAction, but not a MonoidAction... the 0/1 cases don't match up right). Moving to DRAFT while I rethink this.

[gallais]

Conor's disembodied voice tells me we should use a non-symmetric infix symbol for this non-symmetric action.

[jamesmckinna]

Conor's disembodied voice tells me we should use a non-symmetric infix symbol for this non-symmetric action.

I'm genuinely torn over this. I understand, appreciate, and even largely agree with, the doctrine (prevalent in WG2.1) that non-symmetric/commutative operations should be given non-symmetric notation. Nevertheless, we don't insist that that a Group operation be given a non-symmetric symbol... even if we do distinguish it as _+_ (or something else 'obviously connoting commutativity') in the AbelianGroup case.

Nevertheless, I think we do ourselves (or else: type theory as a principled metalanguage for the prosecution of such doctrine) a disservice by taking the 'old-fashioned' CFG view of notation not coming a priori with a type attached.

The case here, as more generally in the draft PR on Algebra.Action, is that the point of an action is that it is extending the domain of applicability of a given operation (however symbolised) to the structure on which it acts... and the generalised associativity property of a MagmaAction is precisely where the extended notation bites, visually/mnemonically at least.

You might object that the Bool action defined here, or Algebra.Definitions.RawMonoid. _×_ aren't in and of themselves 'commutative'... but that obscures the fact that their flipped counterparts are in fact extensionally equal to these definitions.

So perhaps the way out of the bottle is to tag the symbol with ˡ and ʳ annotations, and use infix symbol positions to record where the tail-recursive accumulator argument should go in the extended notation, yielding four compound symbols in all?

I guess I could live with that... modulo leaving _×_ unchanged as 'legacy' (yuk)?

[JacquesCarette]

What prevents this from losing its DRAFT status?

[jamesmckinna]

What prevents this from losing its DRAFT status?

Off the top of my head:

• no bandwidth to think about the problem... incl revisiting
• does it solve the problem I wanted it to?
• does it help with #2457 as I had hoped?

All of the above are slightly beyond my capacity to think right now, so DRAFT seemed to safest way to mark "I'll come back to this (at some point)"

[jamesmckinna]

Notes to self (and any other interested parties here):

• #2892 provides more primitive infrastructure for definitions such as those given here?
• wreath product constructions cf. #2351
• ... 'actions induced by homomorphisms' more generally

It may well be that this all needs reorganisation down the road, at which point it may be clearer (than it is to me now) what would be necessary/useful to isolate 'sensible' common abstractions.