dagger 2-preorder > history in Homotopy Type Theory