HoTT Mini-Course > history in Homotopy Type Theory