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

Preview

Text TheStructure.pdf - Accepted Version Download (519kB) | Preview

Abstract

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
Creators:	Creators Email ORCID Corfield, David Neil d.corfield@kent.ac.uk
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
URI:	https://philsci-archive.pitt.edu/id/eprint/13448

Available Versions of this Item

• Expressing ‘The Structure of’ in Homotopy Type Theory. (deposited 15 Jan 2016 18:47)
  • Expressing ‘The Structure of’ in Homotopy Type Theory. (deposited 21 Sep 2017 19:01) [Currently Displayed]

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item