HoTT/HoTT — pull request #59 by andrejbauer (2013-01-30 21:58:06+00:00)
Title: Added a convenience file theories/HoTT.v which exports the rest of the librarary

A development based on the HoTT library can now import most, if not all of it
by "Require Import HoTT".