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.

agda-stdlib/src/Data/List/Relation/Unary/Grouped/Properties.agda

Line 37 in 8da085e

map⁺ : ∀ {f xs} → (∀ {x y} → P x y ⇔ Q (f x) (f y)) → Grouped P xs → Grouped Q (map f xs)

[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).