PhD position in Homotopy Type Theory