Reorganised some of the basic files using *-Core.agda files.  Added a Vector.agda file to test definition of dependent product.