Synthetic G-jet-structures in modal homotopy type theory

Abstract

This article constructs the moduli stack of torsionfree $G$-jet-structures in homotopy type theory with one monadic modality. This yields a construction of this moduli stack for any $\infty$-topos equipped with any stable factorization systems. In the intended applications of this theory, the factorization systems are given by the deRham-Stack construction. Homotopy type theory allows a formulation of this abstract theory with surprising low complexity. This is witnessed by the accompanying formalization of large parts of this work.

48 pages

References in corpus (9)

• Differential cohomology in a cohesive infinity-topos
• Principal infinity-bundles -- General theory
• Fivebrane Structures
• Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
• Modal Descent
• Synthetic geometry of differential equations: I. Jets and comonad structure
• Modal Fracture of Higher Groups
• Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory
• A Foundation for Synthetic Algebraic Geometry