Polynomials over commutative rings added

[AkermanRydbeck]

Hello,

Here is an implementation of polynomials over commutative rings.

Cheers,
Carl

[mortberg]

Tack så mycket!

[mortberg]

Oops, there is a clash for isZero: https://github.com/agda/cubical/runs/5465312974?check_suite_focus=true

[felixwellen]

You can just hide isZero on import in HornerForms.agda, then everything type checks.

[felixwellen]

And I am really happy we have this definition of polynomials now! And also that it is a set - I didn't know that it works this nicely.

[mortberg]

You can just hide isZero on import in HornerForms.agda, then everything type checks.

Yes, that should be the best solution. @AkermanRydbeck Can you do it please?

[mortberg]

And I am really happy we have this definition of polynomials now! And also that it is a set - I didn't know that it works this nicely.

Yes, I'm also very pleased that we managed to prove that it's a set without truncating. It's very nice to not have to deal with the truncation and to be able to eliminate into arbitrary types.

[AkermanRydbeck]

Hello, glad you like it Felix.

isZero is hidden now.

/Carl