PhilSci Archive

Expressing ‘The Structure of’ in Homotopy Type Theory

Corfield, David Neil (2017) Expressing ‘The Structure of’ in Homotopy Type Theory. [Preprint]

This is the latest version of this item.

TheStructure.pdf - Accepted Version

Download (519kB) | Preview


As a new foundational language for mathematics with its very different idea as to the status of logic, we should expect homotopy type theory to shed new light on some of the problems of philosophy which have been treated by logic. In this article, definite description, and in particular its employment within mathematics, is formulated within the type theory.

Homotopy type theory has been proposed as an inherently structuralist foundational language for mathematics. Using the new formulation of definite descriptions, opportunities to express ‘the structure of’ within homotopy type theory are explored, and it is shown there is little or no need for this expression.

Export/Citation: EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL
Social Networking:
Share |

Item Type: Preprint
Corfield, David
Additional Information: To appear in Synthese.
Keywords: homotopy type theory, definite description, structure
Subjects: Specific Sciences > Mathematics
Depositing User: Dr. David Corfield
Date Deposited: 21 Sep 2017 19:01
Last Modified: 21 Sep 2017 19:01
Item ID: 13448
Subjects: Specific Sciences > Mathematics
Date: 12 September 2017

Available Versions of this Item

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item