Added happly to PathOperations.
Added univalence axiom.
In presence of univalence, universe is not a set.
Updated Everything module.