Cartan Geometry in Modal Homotopy Type Theory