Add two more kinds of duals

The identifiers L and R refer to which ^op is removed/inverted.
Add generalized version of identity functor

Necessary to get between two identical functor categories which use
different instances of funext.