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.
Given an operation (function) , an element of is called a left identity for if for every element of . That is, the map given by is the identity function on .
If , then there is a similar concept of right identity.
If , then is a two-sided identity, or simply identity, if it is both a left and right identity.
Identity elements are sometimes also called neutral elements.
Historically, identity elements (as above) came first, then identity functions, and then identity morphisms. These are all the same basic idea, however: an identity morphism is an identity element for the operation of composition.
An identity is also called a neutral element or sometimes a unit (although that term also has a broader meaning, and an operation that has an identity element is called unital or unitary). In particular, a magma whose underlying operation has an identity is called a unital magma or a unitary magma.
Similarly, a unit law is the statement that a given operation has an identity element. In higher category theory, we generalise from the property of uniticity/unitality to the structure of a unitor.
Last revised on April 5, 2023 at 15:42:03. See the history of this page for a list of all contributions to it.