Move Fibrations.v out of Basics & add stuff using Types.Sigma

I propose that we move `Fibrations.v` out of `Basics`.  I was never entirely sure whether it should be there, but I put it in because it didn't at the time use anything in `Types`.  Now that most of what was there is subsumed by `Types.Sigma`, it seems like `Fibrations` would be a good place to put some other stuff, most of which would be best proven by using `Types.Sigma`.  So let's move it out of `Basics` so it can depend on `Types.Sigma`.

This commit also adds a few things to `Types.Sigma` and `Types.Paths` that were needed for the stuff I wanted to add to `Fibrations`.