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

点击翻译按钮获取中文摘要

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.