Formalizing Cartan Geometry in Modal Homotopy Type Theory

Both, the category of smooth manifolds and the category of schemes may be faithfully embedded in categories of (higher) sheaves on appropriate sites. Homotopy Type Theory is used to reason about those objects and following a suggestion from Urs Schreiber, a modality given by axioms, is used to access the differential geometric structure of the sheaves.
This allows the definition of a notion of infinitesimal proximity, admitting intuitive reasoning on the type theory side. A theorem which forms the basis of what could be called Cartan Geometry is proven, generalizing classical theorems for smooth manifolds. Morphism properties resembling the notions of formally étale, smooth and unramified morphisms from Algebraic Geometry are derived from the notion of infinitesimal proximity and used to define and study spaces locally modeled on a class of types subsuming infinity-groups, vectors spaces and H-spaces. This culminates in the definition of torsion free G-structures.