Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
8906101 | Indagationes Mathematicae | 2018 | 15 Pages |
Abstract
Around 2005, researchers noticed that the rules of type theory also admit homotopy-theoretic models, and subsequently extended type theory with constructs inspired by these models: higher inductive types and Voevodsky's univalence axiom. Although the resulting homotopy type theory has proved useful for homotopy-theoretic reasoning, it lacks a constructive interpretation. In this overview, we discuss a cubical generalization of the meaning explanations of type theory that constitutes an inherently constructive account of higher-dimensional structure in types.
Related Topics
Physical Sciences and Engineering
Mathematics
Mathematics (General)
Authors
Carlo Angiuli, Robert Harper,