[logic-ml] cubical type theory