Skip to main content

Expressing ‘The Structure of’ in Homotopy Type Theory

Corfield, David (2017) Expressing ‘The Structure of’ in Homotopy Type Theory. Synthese, . ISSN 0039-7857. E-ISSN 1573-0964. (doi:10.1007/s11229-017-1569-7) (KAR id:63390)

PDF Publisher pdf
Language: English


Download (522kB) Preview
[thumbnail of 10.1007%2Fs11229-017-1569-7.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF Author's Accepted Manuscript
Language: English
Download (279kB) Preview
[thumbnail of TheStructure.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
https://doi.org/10.1007/s11229-017-1569-7

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.

Item Type: Article
DOI/Identification number: 10.1007/s11229-017-1569-7
Uncontrolled keywords: Structuralism · Definite description · Homotopy type theory · Mathematics
Subjects: B Philosophy. Psychology. Religion > B Philosophy (General)
Divisions: Divisions > Division of Arts and Humanities > School of European Culture and Languages
Depositing User: David Corfield
Date Deposited: 13 Sep 2017 08:22 UTC
Last Modified: 16 Feb 2021 13:48 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/63390 (The current URI for this page, for reference purposes)
Corfield, David: https://orcid.org/0000-0003-0432-3221
  • Depositors only (login required):

Downloads

Downloads per month over past year