This issue of Mathematical Structures in Computer Science is Part I of a Special Issue dedicatedto the emerging field of Homotopy Type Theory and Univalent Foundations.Homotopy Type Theory, as an area of endeavor, studies homotopical interpretations of typetheories, and the synthetic (or syntactic) study of homotopical constructions in type theory.The scientific origins of this field are diverse: milestones include Per Martin-Löf ’s, and ThierryCoquand and Gérard Huet’s, developments of a foundation of mathematics based on dependenttypes, Martin Hofmann and Thomas Streicher’s model of type theory in groupoids, and VladimirVoevodsky’s extension of that model to one in Kan complexes. This last discovery marks the birthof Homotopy Type Theory and based on it, Voevodsky designed his Univalent Foundations asan equivalence-invariant foundation of mathematics; any construction and property in UnivalentFoundations should automatically transfer along a suitable notion of equivalence. As an implementationof this foundation, Voevodsky used type theory for the syntax, and the model in Kancomplexes as the intended semantics.
展开▼
