arXiv · 1806.05966
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.
Explore related subjects
Keep this discovery
Felix Cherubini. 2018-06-15. Synthetic G-jet-structures in modal homotopy type theory. https://doi.org/10.1017/s0960129524000355
Cite the original work for its findings. Save a collection to share your selection of sources.