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