[ refactor ] name of Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable

[jamesmckinna]

Yet another item from #2846 .

NB. There's maybe an argument for saying that this should really consist of:

• rename Pointwise to _×_ (because this is 'merely' a lifting to Binary relations of the underlying Nullary combinator)
• rename ×-decidable to _×?_ (in some sense: ditto.)

UPDATED: now have done so.

[JacquesCarette]

I agree with your really. Feels like this intermediate step is not needed, we should just go to the 'proper' names.

[Taneb]

If we rename Pointwise to _×_, how would we import the module qualified where we currently would have both Data.Product and Data.Product.Relation.Binary.Pointwise.NonDependent imported?

[gallais]

Should it be called All for uniformity?
That's what the pointwise lifting over inductive families is typically called.

[Taneb]

@gallais that's only so far for unary relations, right? This is far more analogous to Data.List.Relation.Binary.Pointwise for me (the notion of decidability for which is just called decidable!)

[jamesmckinna]

OK, thanks for piling in...

@Taneb regarding the choice of names, this is (was) intended to be one more chipping away at renaming X-decidable proofs to X?, so if Data.List.Relation.Binary.Pointwise needs to be updated, it always could be downstream (but if not, then as with #2955 I'm still torn as to whether this really is a good idea, so we should decide that first... on the issue perhaps!?)

@gallais your renaming suggestion for Pointwise makes sense to me, but then I find it hard to confidently arbitrate between the two heuristics:

• uniformity: there's a single name for this concept wherever it appears, as a... lifting of the container functor to predicates, relations... I guess is the intuition?
• name-fidelity: this is an arity-raising operation from Nullary to Binary (and then: why do we do it differently for Unary predicates?)

On the first suggestion, I guess that All/Any might be a way to go (but then I'd double down, and say why don't we use \box/\diamond instead?

I appreciate @JacquesCarette support for my suggestion, but I'd probably rather fix this up downstream, after we have had a 'proper' discussion on a separate issue?

UPDATED: no, let's just do this now.

[jamesmckinna]

As to how to import these things qualified, I'd be OK with

import ...Product.Base as Product using (...)
import ...Pointwise as Pointwise using (...)

and then distinguishing Product._×_ from Pointwise._×_?

UPDATED: or else, as on master now in certain modules, with a renaming (_×_ to _×ᴿ_) directive on imports of Pointwise...

[jamesmckinna]

Aaaargh/A-ha: in Data.Product.Base, we already have, at too specialised a type to capture Pointwise, but nevertheless an instance of the construction:

_-×-_ : (A → B → Set p) → (A → B → Set q) → (A → B → Set _)
f -×- g = f -⟪ _×_ ⟫- g

Should we also consider deprecating this? Or generalising it and using this name instead?

NB this definition is (essentially) the pullback of _×_ along the diagonal maps for A and B, so might be refactorable via On... another time perhaps!

[jamesmckinna]

This, and all subsequent such definitions, could be elided as Carrier never has to be explicitly defined for RawX bundles, because inferrable from _≈_.

So removing these would also 'simplify' these modules, but perhaps at a slightly higher cognitive load wrt intelligbility/legibility?

[jamesmckinna]

Similarly, here, the carrier of the Rel is inferrable from its definition...