Homotopy Type Theory Higher-Dimensional Types in the Mechanization of Homotopy Theory > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Higher-Dimensional Types in the Mechanization of Homotopy Theory < , Higher-Dimensional Types in the Mechanization of Homotopy TheoryKuen-Bang Hou (Favonia), Ph. D. Thesis 2017

Abstract

Mechanized reasoning has proved effective in avoiding serious mistakes in software and hardware, and yet remains unpopular in the practice of mathematics. My thesis is aimed at making mechanization easier so that more mathematicians can benefit from this technology. Particularly, I experimented with higher-dimensional types, an extension of ordinary types with a hierarchy of stacked relations, and managed to mechanize many important results from classical homotopy theory in the proof assistant Agda. My work thus suggests higher-dimensional types may help mechanize mathematical concepts.

See also

category: reference

Last revised on June 9, 2022 at 17:52:34. See the history of this page for a list of all contributions to it.