Homotopy Type Theory together with a monadic modality can be interpreted in an ∞-topos equipped with a stable factorization system. In the examples of interest, the factorization system will be generated by a reflection. We show how an approach to Cartan Geometry, developed by Urs Schreiber, can be implemented on the type theory side of this abstract setup.