Constructive model of homotopy type theory in higher groupoids
Abstract
Type theory is a constructive language for mathematics as well as a functional programming language with a powerful typing system. Due to its effective interpretability, it has been successfully used to specify and prove properties of complex software. Homotopy type theory extends type theory with powerful principles for reasoning about identifications between objects. Its intended semantics is in a generalization of sets called higher groupoids (also known as homotopy types or anima), a higher-dimensional version of equivalence relations that are key to several areas of modern mathematics. One of the main problems of the field is to build an effective (executable) such interpretation. This would allow homotopy type theory to be used as a programming language for homotopy types. However, all previous attempts at this have fallen short of the goal. This project will investigate a new approach to interpret homotopy type theory effectively in higher groupoids, based on a combination of semisimplicial and cubical techniques. We will also examine further possibilities opened up by this result, in particular new constructive models of higher categories.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Feb 06, 2025
- Source ID
- FA95502410302
Entities
People
- Christian Sattler
Organizations
- Air Force Office of Scientific Research
- United States Air Force