Homotopy Type Theory: what can logic do for homotopy theory? - Peter Lumsdaine