HoTTDiTop: Homotopy Type Theory and Directed Topology
Abstract
This proposal concerns the common ground between two recent and exciting ways in which the mathematics of the qualitative (topology) impacts applications. The first --- homotopy type theory --- uses ideas about continuous deformation to explain different ways of proving or guaranteeing results. The second --- applied topology --- concerns the use of qualitative invariants to characterize data sets, signals, and more. The proposed research will generalize and intersect both these branches through notions of directedness. As with the forward orientation of a timeline, a space can be encoded with a direction that constrains motion through that space. Many phenomena are equipped with a natural notion of directedness (such as concurrency, rewriting, neural networks, sensing, and more) or can be equipped with such when observed evolving in time. We seek to develop directed methods, extending both homotopy type theory and applied algebraic topology, to study these phenomena. Our proposal consists of several interrelated objectives. We will establish a truly directed homotopy theory to serve as the semantics of directed homotopy type theory. We will also develop the syntax of the directed homotopy type theory, using modal techniques. We will investigate directed univalence in the type theory and cubical analogues in which directed univalence can emerge. We will develop a novel form of positive homology over a directed space taking values in a category of positive cones, with the goal of setting up a positive persistent homology. This will further develop into a theory of cellular sheaves and cosheaves taking values in categories of positive cones for directed spaces amenable to computation. Finally, we will formalize these theories in order to mechanically verify the results.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 21, 2022
- Source ID
- FA95502110334XX0
Entities
People
- Robert Ghrist
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Pennsylvania