_A Cubical Approach to Synthetic Homotopy Theory_. [[Dan Licata]] and [[Guillaume Brunerie]], LICS 2015 ## Abstract Homotopy theory can be developed [[synthetic homotopy theory|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 Homotopy Theory|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. ## Links * [PDF from Dan's homepage](http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf) * [PDF from Guilluame's homepage](https://guillaumebrunerie.github.io/pdf/lb15cubicalsynth.pdf) category: reference