Done with references HoTTBook, Ch.2 -> library. 

Important links that are missing are: 2.1.8 (loop space), 2.13.1 (paths in nat), 2.15.7 (ac equivalence)