Homotopical Macrocosms for Higher Category Theory

更高范畴理论正越来越多地被用作几个数学领域新结果的元理论，这为主要技术专长位于另一个领域的数学家创造了巨大的进入障碍。过去，PI的联合工作重新设想了无限维范畴理论的基础，目的是通过用适用于任何模型的“合成”方法取代依赖于无限维范畴的特定模型的组合学的“解析”方法来简化证明。这个项目的一个部分试图开发一种计算机可验证的形式语言，它只表达关于无限维类别的声明，这些类别在模型变化时是不变的。这样的语言将通过保证他们表达的每一句话都是与模型无关的，迫使用户“不说坏话”。这个项目与在新提出的单价数学基础系统中重塑无限维范畴理论的计划相联系，在该系统中，直到可收缩的选择空间的同伦唯一性成为真正的唯一性，从而允许对基本概念的简化定义。这两个项目都将与约翰·霍普金斯大学国际和平研究所的学员一起进行。同时，PI有具体的计划继续她的说明性和外展工作，包括一本新书(与Verity联合出版的《无限-范畴理论的元素》)，面向普通公众的讲座，为各种受众准备的调查文章，以及努力改善获得高等数学的机会，例如她在Banff国际研究站的公平、多样性和包容咨询委员会的服务。同伦型理论的先驱-新提出的单价基础系统-设想了无限维范畴理论的计算机可验证基础，但一些计算内容因经典同伦理论中使用的经典推理而丢失。与合作者一起，PI将在一类特定的立方体集合中为经典同伦理论开发一个新的模型，其中立方体纤维要求是等变的，尊重通过置换立方体的维度定义的立方体的对称性。一个更长期的目标是使用类似的方法来获得所有无穷大拓扑的基于立方集的表示。一个基于等变立方纤维的计算机证明助手将具有正确的经典语义，但将能够将计算内容恢复为单价数学。最后一个项目是探索高级范畴理论的同伦宏观宇宙，目的是证明(无穷大，n)-范畴之间的笛卡尔纤维集合组装成(无穷大，n+1)-范畴的笛卡尔纤维，这可以被视为(无穷大，n)-范畴理论的某种范畴化超理论。这种性质的结果将建立针对同伦连贯图的全局提升性质，这应该有助于(无穷大，n)范畴理论的进一步发展。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Higher category theory is increasingly being used as the metatheory for new results in several areas of mathematics, creating a huge barrier to entry for mathematicians whose primary technical expertise lies in another field. Past joint work of the PI reimagined the foundations of infinite-dimensional category theory with the aim of simplifying proofs by replacing "analytic" methods, that rely on the combinatorics of a particular model of infinite-dimensional categories, with "synthetic" ones that apply in any model. One part of this project seeks to develop a computer-verifiable formal language that expresses only statements about infinite-dimensional categories that are invariant under change of model. Such a language would force users to "speak no evil" by guaranteeing that every statement they express is model-independent. This project connects to the plans to recast the theory of infinite-dimensional categories in a new proposed univalent foundation system for mathematics, in which homotopical uniqueness up to a contractible space of choices becomes genuine uniqueness, permitting streamlined definitions of fundamental concepts. Both of these projects will be undertaken in part with mentees of the PI at Johns Hopkins. In parallel, the PI has concrete plans to continue her expository and outreach work which include a new book (Elements of Infinity-Category Theory, joint with Verity), lectures directed at the general public, survey articles prepared for a variety of audiences, and efforts to improve access to advanced mathematics, such as her service on the Equity, Diversity, and Inclusion Advisory Board at the Banff International Research Station.The pioneers of homotopy type theory - the new proposed univalent foundation system - envisioned a computer-verifiable foundation for infinite-dimensional category theory, but some computational content is lost through the classical reasoning used in classical homotopy theory. With collaborators, the PI will develop a new model for classical homotopy theory in a particular category of cubical sets, in which cubical fibrations are required to be equivariant, respecting the symmetries of cubes defined by permuting their dimensions. A longer-term aim is to use similar methods to obtain cubical set based presentations of all infinity-topoi. A computer proof assistant based on equivariant cubical fibrations would have the correct classical semantics but would be able to restore the computational content to univalent mathematics. A final project explores homotopical macrocosms for higher category theory, aiming to prove that the collection of cartesian fibrations between (infinity,n)-categories assemble into a cartesian fibration of (infinity,n+1)-categories, which can be regarded as some sort of categorified hyperdoctrine for (infinity,n)-category theory. Results of this nature would establish a global lifting property against homotopy coherent diagrams that should aid further developments in (infinity,n)-category theory.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.