transfer between mv_polynomial unit and polynomial

Stream: general

[Johan Commelin]

Suppose I want to build a slick machine to move back and forth between mv_polynomial unit and polynomial. Does it make sense to start with

def rel_unit {X : Type u} : (unit → X) → X → Prop :=
λ f x, f unit.star = x

More generally, what goes into building a "transfer API"?

[Chris Hughes]

I thought about this a bit, and I think the function should take an element of an indexing type as an argument. I think this makes it easier if I want to multiply two univariate polynomials together to get a MV poly in two variables.

[Chris Hughes]

I think the transfer API just has all the lemmas about preserving evaluation, degree, multiplication etc.