[ refactor ] Simplify Data.List.Relation.Binary.Lex.NonStrict.<-asymmetric

[jamesmckinna]

Current version:

    <-asymmetric : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
                   Antisymmetric _≈_ _≼_ → Asymmetric _<_
    <-asymmetric eq resp antisym  =
      Strict.<-asymmetric sym (Conv.<-resp-≈ _ _ eq resp)
                        (Conv.<-asym _≈_ _ antisym)
                        where open IsEquivalence eq

only uses the sym : Symmetric _≈_ property from IsEquivalence, so this lemma is unnecessarily restrictive.

Suggest: refactor to streamline the type (breaking), unless we regard the above as a bug?

More generally, it seems as though the List and Vec versions of Lex might benefit from a more thorough reorganisation/refactoring to simplify their (common, but different!) structure and dependencies, but I'm still looking at this cf. #2671

[jmougeot]

I tried to make the change, but it actually requires a deeper modification since Conv.<-resp-≈ relies on transitivity:
<-respʳ-≈ sym trans respʳ, <-respˡ-≈ trans respˡ.

This is absolutely necessary in the function:

<-asymmetric : Symmetric _≈_ → _≺_ Respects₂ _≈_ → Asymmetric _≺_ → Asymmetric _<_ <-asymmetric sym resp as = asym where irrefl : Irreflexive _≈_ _≺_ irrefl = asym⇒irr resp sym as ...

We could change IsEquivalence to PartialEquivalence, but I don’t think we would gain anything from it.

[jamesmckinna]

Thanks @jmougeot for the fine-grained analysis!
In fact, looking also at the Vec versions of these properties, where care is taken to distinguish IsPartialEquivalence from IsEquivalence, I do think the change is worth it. But after your efforts on #2671 I'm very much of the opinion that we should try to do a wholesale reorganisation of Lex for each of List and Vec, to try to identify, as far as possible, a 'common' API. cf. #2682 etc.