Does Identity Make Sense?

Abstract In this paper we present novel conceptions of identity arising in and motivated by a recently emerged branch of mathematical logic, namely, Homotopy Type theory (HoTT). We consider an established 2013 version of HoTT as well as its more recent generalised version called Directed HoTT or Directed Type theory (DTT), which at the time of writing remains a work in progress. In HoTT, and in particular in DTT, identity is not just a relation but a mathematical structure which admits for an interpretation in terms of Homotopy theory (directed Homotopy theory in the case of DTT), which in its turn is supported by common intuitions concerning identity of material objects through time, change and locomotion. The DDTbased conception of identity presented in the paper is nonsymmetric: here identity is “directed” or has a “sense”. We compare the HoTT-based conceptions of identity with standard theories of identity based on the Classical Predicate calculus, and show how the HoTT-based identity helps to treat traditional logical and philosophical problems related to identity and time. In the concluding part of the paper we explore some ontological implications of the HoTT-based identity and show how HoTT and DTT can serve for designing formal process ontologies. The paper is self-contained and comprises expositions and informal explanations of all relevant philosophical, logical and mathematical contents.