Fixed definition of Suspension as per #122.
cleaning up
Added some lemmas.
sync
Merge branch 'master' of https://github.com/HoTT/HoTT
Merge pull request #125 from kristinas/master

Added some lemmas
Sync
Merge branch 'master' of https://github.com/HoTT/HoTT
Added [Misc.v] for miscellaneous lemmas.
Minor comment additions.
Merge branch 'master' of https://github.com/HoTT/HoTT
Renamed lemmas [nullhomot_susp_from_paths].
Resolved #124: renamed [Equivalences.isequiv_cancelR] to [cancelR_isequiv] etc.
Merge pull request #126 from peterlefanulumsdaine/master

Progress on several issues raised yesterday.
sync
Merge branch 'master' of https://github.com/HoTT/HoTT
Added some lemmas.
Merge pull request #128 from kristinas/master

Added lemmas on equivalences: [other_adj], [equiv_ap_l].
Solving universe conflicts
Debug issig2 in Record.v
Merge pull request #130 from SkySkimmer/master

minor debug
Change a Notation into an alias

It doesn't need to be a keyword, and this lets us redefine "unit_name",
should we ever want to.
Merge pull request #132 from JasonGross/notation-to-alias

Change a Notation into an alias