Univalence and Constructive Identity
arXiv:1206.1769
Abstract
The non-standard identity concept developed in the Homotopy Type theory allows for an alternative analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities and accounts for the constructive aspect of such judgements.
5 pages, no figures; presented at the conference "Philosophy, Mathematics, Linguistics: Aspects of Interaction 2012" (May 22- 25, 2012, Euler International Institute, Saint-Petersburg)