sigma-frame > history in Homotopy Type Theory