A Cubical Approach to Synthetic Homotopy Theory
| Autor: | Daniel R. Licata, Guillaume Brunerie |
|---|---|
| Přispěvatelé: | Laboratoire Jean Alexandre Dieudonné (JAD), Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: | |
| Zdroj: | 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.19⟩ LICS |
| DOI: | 10.1109/LICS.2015.19⟩ |
| Popis: | International audience; Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths. While some aspects of homotopy theory have been developed synthetically and formalized in proof assistants, some seemingly easy examples have proved difficult because the required manipulations of paths becomes complicated. In this paper, we describe a cubical approach to developing homotopy theory within type theory. The identity type is complemented with higher-dimensional cube types, such as a type of squares, dependent on four points and four lines, and a type of three-dimensional cubes, dependent on the boundary of a cube. Path-over-a-path types and higher generalizations are used to describe cubes in a fibration over a cube in the base. These higher-dimensional cube and path-over types can be defined from the usual identity type, but isolating them as independent conceptual abstractions has allowed for the formalization of some previously difficult examples. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|