Resolves issue #509 and resolves issue #626

[jamesmckinna]

First things first: resolving issue #626 for Data.List.Properties

• changed 'relative' properties to -local
• this needs to be noted in CHANGELOG

Secondly, resolving issue #509 going through and making map-∘ properties etc. have consistent names across the library

• Data.List.Properties
• what/where else? see below, esp. as regards Codata.*

[jamesmckinna]

Additionally,

• Data.List.NonEmpty.Properties
• Data.List.Zipper.Properties
• Data.List.Relation.Binary.Suffix.Heterogeneous.Properties
• Data.Tree.Rose.Properties
• Data.Fin.Substitution.List
• Data.Maybe.Properties

[jamesmckinna]

And what do we do about these?
The relevant property uses the opposite direction of the bisimilarity relation, because map-map-fusion is meant to simplify/create opportunities for simplification, by pushing the function composition inwards. So do we rename to map-∘ or keep as is?

• Codata.Guarded.Stream.Properties
• Codata.Sized.M.Properties
• Codata.Sized.Delay.Properties
• Codata.Sized.Covec.Properties
• Codata.Sized.Colist.Properties
• Codata.Sized.Stream.Properties

That said, for consistency's sake, we could nevertheless rename map-identity in each to map-id.
EDITED: How to proceed? map-map-fusion and map-identity now both deprecated in favour of the 'standard' names.

[JacquesCarette]

You might want to tackle this more incrementally (i.e. don't do map-id changes in this PR).

My impression is that changes like these do show up in CHANGELOG.

Don't know about Codata.

[jamesmckinna]

Re: incremental changes
as in my comment on the (in my mind, at least) coupled issues, I decided to roll the changes up together in a single PR.
Changing map-identity to map-id is arguably a separate change, but theres' no knock-on viscosity in std-lib, so only clients' code need pay attention to the deprecation... and it's still only a deprecation warning; ergo, harmless?

[JacquesCarette]

The benefit of small PRs is that if there's a problem with one thing, most of the pieces can still be merged in, while if it's all in one big one, perfection must be attained before progress happens.

[gallais]

map-map-fusion (...) do we rename to map-∘

I think we should. For uniformity we may want to flip the lemma too but I don't know whether that's pushing it too far.
Then again 2.0 is the right moment to have these kind of breaking changes.

[jamesmckinna]

Thanks @gallais for the prompt about Codata.*. Similarly change map-identity to map-id? But I think at this stage I would not change the order of the equalities. But it's probably tomorrow or Monday now before I'll tackle these in any case...

[jamesmckinna]

I propose marking this as status:ready, while noting that resolving #509 might also entail another renaming to resolve #501.

[MatthewDaggitt]

Looks great, thanks for the PR @jamesmckinna !