Synthetic and Constructive Mathematics of Higher Structures in Homotopy Type Theory
Abstract
The field of Homotopy Type Theory, while barely a decade old, has already achieved an impressive unification of ideas from homotopy theory, higher category theory, constructive mathematics, and computer science. It has introduced new and powerful synthetic approaches to many areas of mathematics and computation, and thereby made higher-structure tools more accessible to a wide usership of mathematicians, more amenable to computer formalization, and more available for the development of certified software. However, while proof assistants are more powerful and easier to use today than a decade ago, they are still largely disconnected from some of the most powerful tools of modern mathematics. Category theory, and more recently higher category theory, permeates more and more areas of mathematics, and is of growing importance as an organizing principle for computer science and other subjects ranging from theoretical physics to electrical engineering and biology. But even providing the basic tools of category theory in a proof assistant has proven challenging. This presents a barrier both to the wider adoption of proof assistants in mathematics and the use of categorical tools in verified programming. Homotopy Type Theory bridges the worlds of proof assistants and higher category theory, incorporating categorical abstractions directly into the formal type theories on which proof assistants are based. The three main components of this new paradigm are the higher-categorical semantics of type theory, computationally adequate higher type theories, and the use of synthetic concepts to capture higher mathematical structures. This project assembles a team of world-class researchers with expertise in one or more of these three areas. Our goal is to combine our skills to address the current major open problems, thereby fully realizing the potential of Homotopy Type Theory for the synthetic and constructive mathematics of higher structures.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Feb 25, 2023
- Source ID
- FA95502110009
Entities
People
- Michael Shulman
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of San Diego