Add cartesianProductWith⁻ and cartesianProduct⁻ to All

[javierdiaz72]

This PR adds cartesianProductWith⁻ and cartesianProduct⁻ to Data.List.Relation.Unary.All.Properties.

[JacquesCarette]

A few nitpicks.

[JacquesCarette]

There is no point right-indenting so much, go ahead and only indent the type by 2-4 spaces, so as to use fewer lines

[jamesmckinna]

Also: no need for the explicit quantifiers for f and xs/ys in this type?
(But there seems to be no explicitly documented consensus on how much detail of such kind we expect in a CHANGELOG entry...?)

Indeed, are you sure that xs/ys even need to be explicitly quantified at all here?

[JacquesCarette]

I think it would be nicer the use plain pattern-matching for the x∈x′∷xs argument and then dispatch on with.

Also: is there a way to use equational reasoning instead of rewrite? This proof is far from limpid.

[jamesmckinna]

And rather than use with, as the result of that computation has a single-constructor type, it can be irrefutably matched with a pattern-matching let instead, or even the new using syntax?

[jamesmckinna]

But, if the issue is one of laziness, namely that different projections are used in each branch, then better to use proj₁/proj₂ instead?

[jamesmckinna]

Also: in each case branch, pointless eta-expansion wrt the y∈ys argument...

[jamesmckinna]

The Preserves assumption on f seems suspiciously strong, with its use of propositional equality. In other words the lemmas added seem to be insufficiently generalised. Can you improve matters by making a suitable additional Respects assumption about P?

UPDATED: I think that the 'real' cartesianProductWith⁻ should take into account a Setoid/IsEquivalence structure on the codomain of f... and that f should be suitably Congruent₂ wrt its input arguments, and that result structure... in such a way that when specialised to the Pointwise structure on the product, in the special case of cartesianProduct, such congruence property becomes automatic. Additionally, P should suitably respect such structure.

I think that this is the 'usual' problem with _∧_/ _×_ as a connective: we can present it (Prawitz-style) just in terms of _,_/proj₁/proj₂, but it is 'better' to consider it Gentzen-/Schroeder-Heister- style in terms of _,_ and a left rule which is more like pattern-matching let, with result type/conclusion in 'general position' as arbitrary proposition C. The extension to considering Setoid lifting of these concepts seems to demand that we take the more general option?