Kuen-Bang Hou (Favonia) > history in Homotopy Type Theory