Make [Functor] a primitive projection

This gets rid of the remaining variants of duals, and gives us a 20% speedup.

Do we want to merge this now, or wait for [bug 3610](https://coq.inria.fr/bugs/show_bug.cgi?id=3610) and [bug 3619](https://coq.inria.fr/bugs/show_bug.cgi?id=3619) to be fixed?