[DRY] Refactor the various definitions of 'pointwise' equality on functions/Functions/pointwise Algebras

[jamesmckinna]

The upcoming v2.1 has (more or less) standardised on a definition of pointwise equality/relations on (simply-typed) functions as being given by explicit quantification on its domain argument #2400 #2429 (following on from #2240 #2381 #2382 etc.).

This issue is to consider a wholesale refactoring of these definitions (and any other related ones such as Function.Indexed.Relation.Binary.Equality) to introduce them as instances of a common case, namely the 'constant indexed family' version of Relation.Binary.Indexed.Homogeneous.Core.Lift

Follow-up from #2400

[MatthewDaggitt]

I'd be happy to replace them where it's backwards compatible... The problem is that many of them are defined as records or datatypes right? Which as experience has shown have very different inference behaviour from the generic version you link to.

[jamesmckinna]

I'd be happy to replace them where it's backwards compatible... The problem is that many of them are defined as records or datatypes right? Which as experience has shown have very different inference behaviour from the generic version you link to.

Sigh... I guess you're right. :sadface: