equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
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 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é
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
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)
Last revised on December 22, 2019 at 17:18:30. See the history of this page for a list of all contributions to it.