You are here
DigiNole Home » Research Repository » Division of Undergraduate Studies » Undergraduate Honors Theses
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_uhm0304 (IID)  
Keywords:  mathematics, logic, homotopy, computer science  
Submitted Note:  A Thesis submitted to the Department of Mathematics in partial fulﬁllment 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_uhm0304  
Restrictions on Access:  http://creativecommons.org/licenses/byncsa/4.0/  
Owner Institution:  FSU  
Is Part of Series:  Honors Theses. 
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_uhm0304