[logic-ml] from categories to homotopy theory