Feature: Special-case types definable through just polynomial functors

[alexkeizer]

If a (co)inductive type does not involve quotients, then we don't need the full power of QPF's, PFunctors suffice. Polynomial functors have nicer def-eqs, so it would be nice if we could special case this.

Concretely, consider the type of infinite streams

codata (a : Type) Stream 
  | cons : a -> Stream a -> Stream a

We'd like this to satisfy the obvious def-eq. The current definition, in terms of MvQpf.Cofix does not, but an alternative definition in terms of MvPFunctor.M should!

example (s : Stream a) : Stream.cons (s.head) (s.tail) = s := rfl