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 expecially useful for developments building on top of this
library which simply [Import HoTT] and want to prove contractibility
facts in an automated fashion.