Modalities in Homotopy Type Theory