An |x| somehow got lost. It has been retrieved now.
Wrote some stuff on |transport| and everything.
Typo in comments.
Wrote some stuff for HoTT intro.