infinity-group > history in Homotopy Type Theory