fixity of ~ added.
Sigma type as a record.
added a module for univalence.