Saved in:
Bibliographic Details
Main Author: Cherubini, Felix
Format: Preprint
Published: 2018
Subjects:
Online Access:https://arxiv.org/abs/1806.05966
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866915144826617856
author Cherubini, Felix
author_facet Cherubini, Felix
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_1806_05966
institution arXiv
publishDate 2018
record_format arxiv
spellingShingle Synthetic G-jet-structures in modal homotopy type theory
Cherubini, Felix
Differential Geometry
Algebraic Geometry
Category Theory
58A15
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.
title Synthetic G-jet-structures in modal homotopy type theory
topic Differential Geometry
Algebraic Geometry
Category Theory
58A15
url https://arxiv.org/abs/1806.05966