Homotopy theory, homotopy type theory and higher topos theory

同伦理论、同伦类型理论和更高层次的拓扑理论

• 批准号: RGPIN-2022-04739
• 负责人: Christensen, JDaniel
• 金额: $ 1.75万
• 依托单位: University of Western Ontario
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=758495
• 关键词: Homotopy; theory; homotopy; type; higher

My research involves topology, algebra, logic, computation, and various topics in between. Topology is the study of surfaces and higher-dimensional shapes, and the ways in which they can be stretched, deformed and mapped into each other. We study such spaces by probing them with loops, spheres and other simple geometric shapes. This generally results in algebraic invariants which provide qualitative and computational information about a space. Topology has applications in many other fields, such as algebra, data science, physics and computer science. There are many questions and techniques that make sense in all of these settings, and the main theme of my work in topology is the study of such interdisciplinary problems. This interplay between disciplines has proven to be extremely fruitful, often providing insight that leads to solutions to open problems. I will continue to tackle such problems, with a focus on problems involving topology, algebra and geometry. Recently it has been discovered that there is a close connection between topology and logic. Type theory is a foundation for mathematics that has been studied by logicians and computer scientists since the 1970s, and we now know that it is intimately related to topology, in a deep and important way. Part of my work involves studying this relationship between topology and logic and using it to understand both subjects at a more fundamental level. One of the key features of type theory is that proofs done in this framework can be formally verified by a computer to be correct. This is useful both for ensuring correctness of traditional mathematical proofs, and also for verifying the correctness of safety critical software. Some very important results have been formally verified, increasing our confidence in the mathematical literature. In the future, I expect most mathematics to be formally verified, and my work in homotopy type theory will contribute to this while also training HQP in these important skills. Formal verification is also in heavy use in industry, e.g. at Airbus, Intel, Toyota and Microsoft.

我的研究涉及拓扑学，代数，逻辑，计算，以及介于两者之间的各种主题。拓扑学是研究表面和更高维度的形状，以及它们可以被拉伸，变形和映射到彼此的方式。我们研究这样的空间，探索他们与循环，球体和其他简单的几何形状。这通常会导致代数不变量，提供有关空间的定性和计算信息。拓扑学在许多其他领域也有应用，如代数、数据科学、物理学和计算机科学。有许多问题和技术，使在所有这些设置的意义，我的工作在拓扑学的主题是研究这些跨学科的问题。学科之间的这种相互作用已被证明是非常富有成效的，往往提供洞察力，导致解决开放的问题。我将继续处理这些问题，重点是涉及拓扑，代数和几何的问题。最近人们发现拓扑学和逻辑学之间有着密切的联系。类型论是数学的基础，自20世纪70年代以来，逻辑学家和计算机科学家一直在研究它，我们现在知道它与拓扑学有着深刻而重要的关系。我的部分工作涉及研究拓扑和逻辑之间的这种关系，并利用它在更基础的层面上理解这两个主题。类型论的一个关键特征是，在这个框架中完成的证明可以通过计算机进行形式验证。这对于保证传统数学证明的正确性和安全关键软件的正确性都是有用的。一些非常重要的结果已经得到了形式上的验证，增加了我们对数学文献的信心。在未来，我希望大多数数学都能得到正式的验证，我在同伦类型理论方面的工作将有助于这一点，同时也训练HQP掌握这些重要的技能。形式验证也在工业中大量使用，例如在空中客车、英特尔、丰田和微软。