Merge pull request #79 from mikeshulman/hset

Shuffle around the locations of some things, eliminate some duplicate lemmas
Adding path_induction
Merge branch 'master' of github.com:HoTT/HoTT
Quickly make Fibrations compile
Adding preliminary version of the hott_simpl tactic
Empty commit after rebasing (???
Functoriality of [forall].
Added [flip] and [isequiv_flip].
Reinstated [equiv_rect], [equiv_intro], accidentally deleted when rebasing.
Added [Trunc_forall].
Added [Trunc_resp_equiv], modulo outstanding lemma [ap_equiv].
Added [ap_equiv]: an equivalence induces an equivalence on paths.
Merge branch 'upstream'