H-magmoid > history in Homotopy Type Theory