[infinite]-Lie Groups and Their [infinite]-Lie Algebras in Real Cohesive Homotopy Type Theory

类型理论长期以来一直是理论计算机科学的基石，为编程语言理论提供了形式化方法[10]。最近，同伦类型理论（HoTT）的发展[9]已经成为纯数学和计算机科学之间的桥梁，将代数拓扑与计算联系起来。HoTT已经被证明是所有（[infinite]，1）-topoi的内部逻辑[8]，这是一大类更高的范畴。给这种类型理论增加额外的结构，特别是以模态的形式，提供了一个更具体的数学环境。Mike Shulman引入了内聚HoTT，将Lawvere [3]和Schreiber [7]的公理内聚思想内化到类型论中。这些新的结构使我们能够访问同伦类型的“几何”结构，从而可以访问微分拓扑和几何中的问题。这项工作是一个更大的项目的一部分，该项目旨在将Schreiber [7]提出的现代物理学的分类基础翻译成HoTT语言。特别是，超引力、弦理论和M理论都可以用这种方式表述。这个项目将继续这一努力，通过专注于高层次群体的差异研究凝聚力HoTT，旨在简化现有的介绍更高的李理论。

Type theory has long been a cornerstone of theoretical computer science, providing the formal methods for programming language theory [10]. More recently, the development of homotopy type theory (HoTT) [9] has served as a bridge between pure mathematics and computer science, relating algebraic topology to computation. HoTT has been shown as the internal logic of all ([infinite], 1)-topoi [8], a large class of higher categories. Adding extra structure to this type theory, in particular in the form of modalities, gives a more specified mathematical setting to work in. Mike Shulman introduced cohesive HoTT to internalise the ideas of axiomatic cohesion, from Lawvere [3] and Schreiber [7], into type theory. These new structures allow us to access the "geometric" structure of a homotopy type, giving access to questions in differential topology and geometry. This effort is part of a larger project to translate the categorical foundations of modern physics presented by Schreiber [7], into the language of HoTT. In particular, supergravity, string theory and M-theory can be formulated in this way. This project will continue this effort, by focusing on the differential study of higher groups in cohesive HoTT, with an aim to simplify the existing presentation of higher Lie theory.