模态同伦类型论中的合成G-射流结构

本文在同伦类型论中带有一个单子模态的情形下，构造了无挠$G$-射流结构的模栈。这给出了对任意装备有任意稳定因子系统的$\infty$-拓扑空间该模栈的构造。在该理论预期的应用中，因子系统由deRham栈构造给出。同伦类型论允许以惊人低复杂性表述这一抽象理论。伴随本工作大部分内容的形式化证明了这一点。