You are here

Overview of Homotopy Type Theory and the Univalent Foundations of Mathematics

Title: An Overview of Homotopy Type Theory and the Univalent Foundations of Mathematics.
77 views
34 downloads
Name(s): Dunn, Lawrence, III, author
Department of Mathematics
Type of Resource: text
Genre: Text
Issuance: serial
Date Issued: 2014
Physical Form: computer
online resource
Extent: 1 online resource
Language(s): English
Abstract/Description: 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.
Identifier: FSU_migr_uhm-0304 (IID)
Keywords: mathematics, logic, homotopy, computer science
Submitted Note: A Thesis submitted to the Department of Mathematics in partial fulfillment of the requirements to graduate with Honors in the Major.
Degree Awarded: Spring Semester, 2014.
Date of Defense: April 24, 2014.
Subject(s): Geometry
Topology
Logic
Mathematical analysis -- Foundations
Mathematics -- Philosophy
Compilers (Computer programs)
Programming languages (Electronic computers)
Persistent Link to This Record: http://purl.flvc.org/fsu/fd/FSU_migr_uhm-0304
Restrictions on Access: http://creativecommons.org/licenses/by-nc-sa/4.0/
Owner Institution: FSU
Is Part of Series: Honors Theses.

Choose the citation style.
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