Dan Licata > history in Homotopy Type Theory