Merge pull request #427 from JasonGross/implicit-equiv

Mark the arguments to Equiv projections implicit
Use primitive projections and eta

This allows us to eliminate various redundancies, such as the manny
variants of duals.

This closes #425.