Instance MvFunctor Prod' is not universe-polymorphic

[Kiiyya]

The qpf macro struggles with universe levels, concretely in conjunction with product types.

qpf F₁ (A : Type 0) B := A × B -- works
qpf F₂ (A : Type 1) B := A × B -- fails

Which gives the following error message:

failed to synthesize
  MvFunctor.{max ?u.2094 1, max ?u.2094 1} (TypeFun.ofCurried.{max ?u.2094 1, max ?u.2094 1} Prod.{1, max ?u.2094 1})

This is likely because the instance is not universe-polymorphic. What we need is instance : MvFunctor.{u, u} MvQPF.Prod.Prod'.{u} := sorry

[Kiiyya]

I also noticed that the IsPolynomial instance for Prod' is not universe-polymorphic either. What we need is instance : MvQPF.IsPolynomial.{u, u} MvQPF.Prod.Prod'.{u} := sorry

[alexkeizer]

We probably ought to get rid of IsPolynomial alltogether, see #53