HoTT/HoTT — pull request #29 by peterlefanulumsdaine (2012-11-13 23:04:51+00:00)
Title: Added lemma [forall_hlevel], that h-levels are closed under arbitrary products.

Added the useful lemma that h-levels are closed under dependent products over arbitrary bases; also made minor changes in a couple of nearby proofs, giving lemmas about h-props as instances of lemmas about h-levels rather than re-proving them directly.