Finish non-dep functoriality of adjoints

With some help from Mike Shulman on #627 and #629, I've managed to
finish the construction that shows that the construction of adjoint
functors is functorial in its functor argument.  I've not yet managed to
extend this to the dependent case as an assembled functor, though the
individual parts all have dependent versions.

This closes #629.
It a compatibility command that allows the old-style `match`-statement.  In 8.4, the default was to not permit the parameters to show up in the arguments (so `cons` took two arguments and `nil` took zero), and in trunk, the default is to require the extra parameters:
```coq
Inductive list A := nil | cons (x : A) (xs : list A).
Unset Asymmetric Patterns.
Definition behead {A} (ls : list A)
  := match ls with
       | nil _ => nil _
       | cons _ x xs => xs
     end.
Set Asymmetric Patterns.
Definition behead' {A} (ls : list A)
  := match ls with
       | nil => nil _
       | cons x xs => xs
     end.
```

Since this is given as a compatibility option, it's possible that (perhaps when we clean up to make an 8.5 release) we should strip this option and adjust all of the explicit matches.

The reason it shows up at the top of files like this was that I'm keeping the styles of the categories files to put these settings at the top of each file.  It's sufficient to globally set them once at the top of `categories/Category/Core.v`.