equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
In philosophy, the statement that given any , then equals
(i.e. reflexivity) has been called (see the references below) the first law of thought.
In terms of type theory this is the judgement that exhibits the term introduction for the reflector in an identity type
In fact, identity types may be regarded as inductive types generated by just this reflector (Licata 11, Shulman 12, slide 35, see there).
In Gottfried Leibniz‘s unpublished but famous manuscript on logic (from some time in 1683-1716), reproduced in the Latin original in
and English translation in
it says, after statement of the identity of indiscernibles and then the indiscernibility of identicals, that
and are, of course, said to be the same
Later,
calls “” “den ersten, schlechthin unbedingent Grundsatz” hence the “absolutely imperative principle”. (In fact Fichte there highlights the importance of the antecedent to arrive at the consequent .)
in its §875 calls it the first original law of thought:
The first original law of thought (WdL §875): everything is identical with itself (WdL §863), no two things are like each other (WdL §903).
in Footnote, p. 38 calls it the first of the four primary laws of thought.
See also
which gives quotes by Arthur Schopenhauer to the same extent.
For the understanding of identity types as inductive types genrated just by the reflector see
Dan Licata, Understanding Identity Elimination in Homotopy Type Theory, 2011
Mike Shulman, around slide 35 of Inductive types and identity types, 2012 (pdf)
Last revised on September 23, 2022 at 16:32:31. See the history of this page for a list of all contributions to it.