[logic-ml] elements of higher category theory