[logic-ml] 2-dimensional categories