port sigma library

Ported a lot of the Coq-HoTT [sigma library](https://github.com/HoTT/HoTT/blob/master/theories/Types/Sigma.v) (up to line 360).

Minor changes elsewhere:
- protect some definitions in `equiv`
- add notation `▹2` `▹D` and `▹D2` for dependent transports and higher transports.
- comment out the `sorry` in `trunc`

Remark: The higher order unification is really nice. I have to give much less information for transports than they do in Coq-HoTT.

(there are still some commented proofs from the Coq library in `types/sigma`. Is that a problem? If so, you can remove them)