Homotopical Macrocosms for Higher Category Theory

高等范畴理论越来越多地被用作数学若干领域新成果的元理论，这给那些主要技术专长在另一个领域的数学家们制造了巨大的进入障碍。PI过去的联合工作重新构想了无限维范畴论的基础，目的是通过用适用于任何模型的“合成”方法取代依赖于无限维范畴特定模型的组合学的“分析”方法来简化证明。该项目的一部分是寻求开发一种计算机可验证的形式语言，它只表达关于在模型变化下不变的无限维类别的陈述。这样的语言将通过保证用户表达的每个语句都是独立于模型的，来迫使用户“不说坏话”。这个项目与在一个新提出的数学单价基础系统中重铸无限维范畴理论的计划相联系，在这个基础系统中，直到可收缩的选择空间的同伦唯一性成为真正的唯一性，允许基本概念的简化定义。这两个项目都将与约翰霍普金斯的PI学员一起进行。与此同时，PI有具体的计划继续她的宣传和推广工作，其中包括一本新书（元素的无穷大类理论，与Verity联合），讲座针对公众，调查文章准备了各种观众，并努力提高获得高等数学，如她的服务公平，多样性，同伦类型理论的先驱--新提出的单价基础系统--设想了一个计算机可验证的无限维范畴理论的基础，但是通过在经典同伦理论中使用的经典推理丢失了一些计算内容。与合作者，PI将开发一个新的模型，经典同伦理论在一个特定类别的立方集，其中立方纤维化需要是等变的，尊重对称的立方体定义置换其尺寸。一个长期的目标是使用类似的方法来获得所有无穷大拓扑的基于立方集的表示。一个基于等变立方纤维化的计算机证明助手将具有正确的经典语义，但能够将计算内容恢复为单价数学。最后一个项目探讨了更高范畴理论的同伦宏观世界，旨在证明（无穷，n）-范畴之间的carnival纤维化的集合组装成（无穷，n +1）-范畴的carnival纤维化，这可以被视为（无穷，n）-范畴理论的某种范畴化的hyperdoctrine。这种性质的结果将建立一个全球提升属性同伦连贯图，应有助于进一步发展（无穷大，n）-categorytheory.This奖项反映了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.