Article ID Journal Published Year Pages File Type
8906101 Indagationes Mathematicae 2018 15 Pages PDF
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
, ,