This implication should work for any setoid-based permutation

[onestruggler]

This implication should work for any setoid-based permutation, not just the equality setoid:

agda-stdlib/src/Data/List/Relation/Binary/Permutation/Propositional.agda

Line 98 in 3880dec

↭⇒↭ₛ : xs ↭ ys → xs ↭ₛ ys

[MatthewDaggitt]

Agreed. Not easy to do in a backwards compatible way unfortunately... Might have to be an additional lemma.

[jamesmckinna]

Hmmm... I think I was originally responsible for these (the one direction requiring the Propositional setoid, the other, correctly as here, being more general, and I didn't have my eye on the ball). As for how we think about this:

• refactoring rather than, or as well as, addition?
• breaking; I'd be tempted simply to break the API for v3.0, or even v2.3 as this was an (unintentional) bug, moreover only introduced recently as part of v2.2?

Alternatively, make the simple addition (modulo map id ≐ id, and the trivial proof that id Preserves _≡_ ⟶ _≈_) to Propositional by composing the above lemma with Setoid.Properties.map⁺ instantiated at {f = id}. Hmmm.