[kisoron-ml] modalities in homotopy type theory