Published in Synthese, (open access). It will be reworked considerably to appear as chapter 3 in my forthcoming book Modal Homotopy Type Theory.
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.
Back to HomePage.
Last revised on November 19, 2019 at 14:05:21. See the history of this page for a list of all contributions to it.