[logic-ml] modalities in homotopy type theory