1: \begin{abstract}

2:     In this article, some Differential Geometry is developed synthetically in a Modal Homotopy Type Theory.

3:     While Homotopy Type Theory is used to reason about general $\infty$-toposes,

4:     the ``Modal'' extension we are using here, is concerned with special $\infty$-toposes with the extra structure

5:     of an idempotent monad with some additional properties.

6:     On the type theory side, the extension is realized by adding well known axioms of a \emph{monadic modality}.

7:     In the applications we have in mind, this monadic modality corresponds to

8:     monads exhibiting infinitesimal information of the objects of special $\infty$-toposes of spaces.

9:     There are two main lines of examples of these toposes, one containing smooth manifolds, the other algebraic varieties.

10:     Since we use Homotopy Type Theory, stacks from both of these worlds are naturally included in our discussion.

11:     We will make use of this in developing some new higher differential geometry.

12:     Much of the higher differential geometry in this article is aimed at making our construction of

13:     moduli spaces of $G$-structures and torsionfree $G$-structures possible in a useful way.

14:     As a basic example, this abstract construction of moduli spaces may be instantiated for a topos containing manifolds

15:     and the orthogonal group to give a construction of the moduli stack of Riemannian Metrics on a smooth manifold.

16:     The $G$-structures are developed along the lines of Urs Schreiber's Higher Cartan Geometry. 

17:   \end{abstract}

18: