[ add ] Pointwise lifting of algebra to Data.Vec.Functional

[JacquesCarette]

This is a partial redo of #2817 for all the Algebra parts. If this seems good, then we can do the Module parts as well.

[jamesmckinna]

Is Base all that there is going to be for this PR? (ie is this ready for review? I guess it must be... you did ask...)

[jamesmckinna]

DRY!!!

The substance of this PR lies in answering the following question: what cannot be achieved by re-export from Algebra.Construct.Pointwise?

[jamesmckinna]

Notwithstanding my use of lift for helper functions in Algebra.Construct.Pointwise, I personally hate the use of Lift as a module name for qualified import. I would much prefer

Suggested change

	import Algebra.Construct.Pointwise as Lift
	import Algebra.Construct.Pointwise as Pointwise

cf. #2280

[jamesmckinna]

If the sole contents of this module are to be the re-exports of the Bundles, then this could be almost entirely shortcircuited (Fairbairn?) as:

Suggested change

	module Data.Vec.Functional.Algebra.Base where
	open import Data.Nat.Base using (ℕ)
	module Data.Vec.Functional.Algebra.Base (n : ℕ) where
	open import Data.Fin.Base using (Fin)
	-- Re-export existing constructions
	open import Algebra.Construct.Pointwise (Fin n) public

And indeed, if there is to be more here, then why not refactor in this style anyway? (in the anonymous module you define below).

I think this was the substance of my critique of #2817 , and my suggestions that the corresponding Module additions be moved to Algebra.Module.Construct.Pointwise #2915 , and, if necessary, be re-exported here on the same basis as above?

[JacquesCarette]

Thanks for pointing out that this should morally be a 1-liner! And in that guise, if additions are made to the Construct module, they would "appear" here automatically as well: win-win.

The question as to whether this is going to be all there is: it depends on whether the Module-related additions should also go in this PR, both infrastructure and deployment. And where the resulting bundles should be deployed from (i.e. this module or another).

I don't think we should ever instantiate a "construction" module inside of itself. So if this module ends up a 1-liner in the end, I'm fine with that.

[jamesmckinna]

Thanks for pointing out that this should morally be a 1-liner! And in that guise, if additions are made to the Construct module, they would "appear" here automatically as well: win-win.

@JacquesCarette

• [ add ] Algebra.Module.Construct.Pointwise, following Algebra.Construct.Pointwise #2915 and my comments on [ add ] Pointwise lifting of algebra to Data.Vec.Functional (Functional vector module #1945 redux) #2817 suggest to me that it's Algebra.Module.Construct where work will be required, cf. [ add ] functorial change-of-base from S-YModule to R-YModule induced by an XRing homomorphism from R to S #2913
• more than happy (modulo Fairbairn) to have the current contribution essentially be a stub for re-export...
• ... and downstream use by the Module stuff...

I await developments!

As for

The question as to whether this is going to be all there is: it depends on whether the Module-related additions should also go in this PR, both infrastructure and deployment. And where the resulting bundles should be deployed from (i.e. this module or another).

I could imagine a similar 'staging': Pointwise constructions on modules, re-exported here for the A = Fin n case, together with... other machinery developed here?

I don't think we should ever instantiate a "construction" module inside of itself. So if this module ends up a 1-liner in the end, I'm fine with that.

Sounds principled!