Use `-local` consistently for properties

[gallais]

In Data.List.Properties we use

• map-id₂ : All (λ x → f x ≡ x) xs → map f xs ≡ xs
• map-cong₂ : All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
• (we do not have map-compose₂)

I think that we should instead use the -relative suffix introduced in #510

[MatthewDaggitt]

What does relative refer to?

[gallais]

The fact the equality constraint is relative to a specific domain (in order to be
as tight a constraint as possible) rather than absolute.

[MatthewDaggitt]

Hmm looking at this again, I'd probably prefer the prefix -locally (or -local) instead of -relative, as in the equality constraints hold locally. Thoughts?

[JacquesCarette]

To be honest, I don't like either -locally or -relative. Isn't this rather a 'lifting' property? You're lifting an equality to hold at a list. In some ways, this is a generalization of ap.

[MatthewDaggitt]

So map-id-lift? I like it better than -relative but less than -local. I'd be fine with it though....

[MatthewDaggitt]

Going to leave this out of v1.0, as I don't think we've reached consensus yet.

[MatthewDaggitt]

@jamesmckinna thinks the suffix should be at e.g. map-id-at

After discussion we're going with local