HoTT/HoTT — pull request #587 by mikeshulman (2014-10-22 05:45:26+00:00)
Title: 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`.