Prefix 'Instance' with 'Global'

`Instance`s are, by default, local to sections.  I've gone through and prefixed all of the `Instance`s inside `Section`s of with `Global`, so they get picked up by typeclass search.  I don't think I missed any, but I'm not sure.
    
This is especially useful for developments building on top of this library which simply `Import HoTT` and want to prove contractibility facts in an automated fashion.

This bit me when trying to do some things in my category theory library.

Once again, my emacs has removed all the trailing spaces from the relevant files.  I can resubmit this pull request without those line changes if desired.

(Note: This is an updated version of the old commit, which only did this for sections labeled `AssumeFunext`.)