add vector and category

Here are my current versions of category.lean and vector.lean. There isn't much in either, but it's a start. It compiles with the current version, so it's updated to use "open" and "." (instead of "include" and "_"). It does use some superfluous sorry's and check's