Adding Nth-polynomials

[thomas-lamiaux]

Adding nth-polynomials using a new definition

[felixwellen]

Interesting! Did you see Cubical/Algebra/CommAlgebra/Instances/FreeCommAlgebra.agda?
I think that is related to what you do. It seems you are a bit more economical with the constructors of your type of polynomials.

Btw: You can mark your pull-request as 'draft'. This is a good way to indicate, that it is work in progress.

[thomas-lamiaux]

Interesting! Did you see Cubical/Algebra/CommAlgebra/Instances/FreeCommAlgebra.agda? I think that is related to what you do. It seems you are a bit more economical with the constructors of your type of polynomials.

I didn't see it even though I am currently working with Anders, I think that they originated very differently.
Basically we were looking for a good definition of the direct-sum. Working with one we've come up with, I have realized that I could define nth-polynomials easily and it would simplify some latter proof.

Plus, I am not a big fan of the current one based on the :: operation. I prefer this one base on "vectorial space". With the difference that the action on the basis is internalized - which comes from the direct sum that is dependent - and seems to facilitate definition and proofs.
Indeed basically it suffices to specify the behavior for aX^n, to define functions such as the product so all structures rises and that simplify the structure.

Btw: You can mark your pull-request as 'draft'. This is a good way to indicate, that it is work in progress.

Indeed I forgot to do it, it's done thanks

[thomas-lamiaux]

Would adding a syntactic sugar like X^n1...X^nk for base [n1, ... nk] 1 be interesting ?

(I don't really know how to do so for any k)

[mortberg]

Also please remove trailing whitespace

[mortberg]

There's still some trailing whitespace:

~/.cabal/bin/fix-whitespace --check
[ Violation detected ] Cubical/Algebra/Polynomials/Univariate/Properties.agda