Identity and intensionality in Univalent Foundations and philosophy

The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not immediately clear how these principles are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional mathematics. Our main purpose will be the philosophical investigation of this system, and the relation of the concepts of intensionality it satisfies to more traditional philosophical or logical concepts such as those of Carnap and Quine.