nLab identity of indiscernibles




The principle of identity of indiscernibles states that two objects are identical if they have all the same properties.

This is also known as “Leibniz‘s Law” (not to be confused with the product rule, also so-called).

In homotopy type theory

In the presence of an identity type, identity of indiscernibles is trivial because of haecceities?; but extensionality principles like function extensionality, propositional extensionality, and univalence (“typal extensionality”) are naturally regarded as a stronger form of identity of indiscernibles. In particular, the consistency of univalence means that in Martin-Löf type theory without univalence, one cannot define any predicate that provably distinguishes isomorphic types; thus isomorphic types are “externally indiscernible”, and univalence incarnates that principle internally by making them identical.

“There are several ways to think about the axiom of univalence. One can see it as a sophisticated updating of Leibniz’s principle of the identity of indiscernibles.” –John Baez nCafé

In topology

A topological or geometrical version of the idea of identity of indiscernibles is separation: if two points are distinct, then they are separated in some sense. This means in turn that if two points in a space subject to a given separation axiom can not be separated by any admissible separation condition then they are identical.


Formalization in homotopy type theory is in

Last revised on December 22, 2019 at 17:18:30. See the history of this page for a list of all contributions to it.