Synthetic G-jet-structures in modal homotopy type theory

TL;DR

This paper develops a framework in homotopy type theory for constructing moduli stacks of G-jet-structures, leveraging monadic modalities and stable factorization systems, with formalization supporting its low complexity.

Contribution

It introduces a novel construction of moduli stacks of G-jet-structures within homotopy type theory using monadic modalities and stable factorization systems.

Findings

Construction of the moduli stack for any ∞-topos with stable factorization systems

Application to deRham-Stack construction in specific contexts

Formalization demonstrating low complexity of the 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.