[ refactor ] Functoriality of Data.List.Relation.Binary.Sublist|Subset wrt All and Any

[jamesmckinna]

Should this be a corollary of something about All P xs implies All P ys whenever ys is a subset of xs?

Indeed, and this appears twice in the library:

• Data.List.Relation.Unary.All.Properties.anti-mono : xs Subset.⊆ ys → All P ys → All P xs (and Sublist is a stronger property than Subset)
• Data.List.Relation.Binary.Sublist.Propositional.Properties.All-resp-⊆ : {P : Pred A ℓ} → (All P) Respects _⊇_ and this should (added: perhaps?) be refactored to a proof in ...Sublist.Setoid.Properties, under assumptions that P respects the underlying Setoid equality?

Originally posted by @jamesmckinna in #2522 (comment)

[MatthewDaggitt]

Eek that's not ideal that it appears twice 😓

My instincts say that it should live under Sublist...

[jamesmckinna]

My instincts say that it should live under Sublist...

As would mine, except for the fact that the Sublist versions morally should delegate to the Subset versions via Sublist⇒Subset? But then we have the problem that this lemma is under ...Subset.Setoid.Properties... sigh!?

[MatthewDaggitt]

As would mine, except for the fact that the Sublist versions morally should delegate to the Subset versions via Sublist⇒Subset?

Err, that's not a principle that any of the existing code has been designed around. It might be possible to do but it would involve a wholesale refactoring of the Sublist modules I suspect.

[JacquesCarette]

(There's quite a bit of discussion in #2522 that is relevant.)

This is a much more general design issue: should we prove things directly or as special cases of more general results? That's probably the real discussion to be having. I'm fairly sure that has come up before! There are pros and cons, and my opinion on that has changed (evolved?) multiple times over the years.