Weaken preconditions of `map` lemmas for `Grouped` predicate

[MatthewDaggitt]

The map lemmas in Data.List.Relation.Unary.Grouped.Properties use functional equivalence rather than relational equivalence, and therefore require a bunch of additional and unnecessary equality constraints.

https://github.com/agda/agda-stdlib/blob/8da085e032ce50db75a7bbb63bfa56bddaf8e4ad/src/Data/List/Relation/Unary/Grouped/Properties.agda#L37

[lexvanderstoep]

Hey Matthew, I started working on this issue, and struggled to get my head around the following: if P is a relation on elements of type A, and Q is a relation on elements of type B, then what would be the type of the relation equivalence?

[gallais]

I think you'd be looking at mutual pointwise implication of P and Q on f where on is defined in Function.Base.

[lexvanderstoep]

Could a bi-implication version of P =[ f ]⇒ Q work as well?

The type of the lemmas would then be along the lines of: map⁺ : ∀ {f xs} → P ⇚[ f ]⇛ Q → Grouped P xs → Grouped Q (map f xs), where P ⇚[ f ]⇛ Q = (P =[ f ]⇒ Q) × (Q =[ f ]⇒ P).