Homotopical inductive types

在过去的几年里，在两个传统上相距遥远的数学领域之间出现了令人惊讶的新联系：数理逻辑(通常涉及数学中使用的推理形式的研究)和同伦理论(感兴趣的是对各种空间概念的理解和分类)。这些联系是有用的，因为它们提供了一种清晰的几何直觉，帮助我们处理一类被称为类型理论的逻辑系统。在此基础上，菲尔兹奖获得者沃沃夫斯基制定了一个雄心勃勃的研究计划，称为单价数学基础计划，该计划寻求在类型理论的基础上发展新的数学基础，其中包括由同伦理论引发的新公理。拟议的研究旨在增进我们对沃沃夫斯基提出的类型理论的理解，以发展单价基础计划。我们的第一个目标是更好地理解沃沃茨基引入的类型理论和公理集合论之间的关系，公理集合论代表了更传统的数学基础方法。特别是，我们想要澄清一价公理的逻辑地位，这是一种新的公理，它允许我们平等地对待拥有所有结构属性的对象。此外，我们还希望对定义类型的标准方式上的一种变体有进一步的了解，这种变体同样是由同伦理论驱动的。

Over the past few years, new surprising connections have emerged between two traditionally distant areas of mathematics: mathematical logic (which is generally concerned with the study of the forms of reasoning used in mathematics) and homotopy theory (which is interested in understanding and classifying various notions of space). These connections are useful because they provide a cleargeometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.