modularize

everything in Categories.v is in a separate module now, so each
such module can become a separate file