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
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Download this file (PDF/468kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
PDF
Author's Accepted Manuscript
Language: English |
|
Download this file (PDF/386kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
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 Culture and Languages |
Depositing User: | David Corfield |
Date Deposited: | 13 Sep 2017 08:22 UTC |
Last Modified: | 05 Nov 2024 10:58 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/63390 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):