nLab identity of indiscernibles

Idea

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.

References

• Wikipedia
• SEP

Formalization in homotopy type theory is in

• Univalent Foundations Project, section 1.12 of Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Ladyman & Presnell (2016) formulate four variants of this principle in homotopy type theory.

• Favonia, appendix B of Higher-Dimensional Types in the

  Mechanization of Homotopy Theory_, PhD thesis 2017, (pdf)