Some of the material in is restricted to members of the community. By logging in, you may be able to gain additional access to certain collections or items. If you have questions about access or logging in, please use the form on the Contact Page.

Dunn, L. (2014). An Overview of Homotopy Type Theory and the Univalent Foundations of
Mathematics. Retrieved from http://purl.flvc.org/fsu/fd/FSU_migr_uhm-0304

Homotopy type theory, the basis of ''univalent foundations'' of mathematics, is a formal system with intrinsic connections to computer science, homotopy theory, and higher category theory. Rooted in type theory, the theoretical basis of most modern proof assistants, the system admits an interpretation as a logical calculus for homotopy theory and suggests a foundational system for which abstract ''spaces'' -- not unstructured sets --- are the most primitive objects. This perspective offers both a computational foundational for mathematics and a direct method for reasoning about homotopy theory. We present here a broad contextual overview of homotopy type theory, including a sufficiently thorough examination of the classical foundations which it replaces as to make clear the extent of its innovation. We will explain that homotopy type theory is, loosely speaking and among other things, a programming language for mathematics, especially one with native support for homotopy theory.

A Thesis submitted to the Department of Mathematics in partial fulﬁllment of the requirements to graduate with Honors in the Major.

Identifier

FSU_migr_uhm-0304

Dunn, L. (2014). An Overview of Homotopy Type Theory and the Univalent Foundations of
Mathematics. Retrieved from http://purl.flvc.org/fsu/fd/FSU_migr_uhm-0304