Univalent Foundations of Mathematics

由Alexander Grothendieck首先猜想的同伦类型与群胚的更高范畴类比之间的对应关系自然导致了一种数学观点，即集合被用来参数化没有“内部结构”的对象的集合，而具有“内部结构”的对象的集合被更一般的同伦类型参数化。单叶基础是基于这一观点和发现的结合，即可以使用Matin-Lof型理论直接形式化关于同伦型的推理。我们期望，这种新的基础方法最终将使数学家在日常工作中使用证明开发软件变得切实可行。几十年来，这种软件(“校对助手”)的复杂性和用户友好性一直在稳步增长，它在计算机科学中的使用正在成为标准。使其在纯数学中的应用将对新一代数学家和整个数学界都有很大的好处。

The correspondence between homotopy types and higher categorical analogs of groupoids, first conjectured by Alexander Grothendieck, naturally leads to a view of mathematics where sets are used to parametrize collections of objects without "internal structure", while collections of objects with "internal structure" are parametrized by more general homotopy types. Univalent foundations are based on the combination of this view with the discovery that it is possible to directly formalize reasoning about homotopy types using Matin-Lof type theories. We expect that this new approach to the foundations will finally make it practical for mathematicians to use proof development software in their everyday work. The sophistication and user friendliness of such software ("proof assistants") have been growing steadily for decades and its use in computer science is becoming standard. Enabling its use in pure mathematics will be of great benefit to the new generations of mathematicians and to the mathematical community as a whole.