My activity on this blog has been reduced to nil recently because I have been spending my time preparing a series of lectures on homotopy type theory, starting from basic principles and ending with the application of univalence and higher inductive types to algebraic topology. The course web page contains links to the video-taped lectures and to the course notes prepared by the students this semester. These will be available indefinitely and are accessible to anyone interested in the course. My hope is that these will provide a useful introduction to the HoTT Book, which is available for free on the web and may be printed on demand. My intention is to write an introduction to dependent type theory for a CS audience, which will serve as a reference for much ongoing work in the area and as a prolegomenon to the HoTT Book itself.
Homotopy Type Theory Lectures and Notes On-Line