Steve Awodey: Homotopy Type Theory. ICLA 2015: 1-10