Redirected from "identity maps".
Contents
Context
Equality and Equivalence
equivalence
-
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
-
natural equivalence, natural isomorphism
-
gauge equivalence
-
Examples.
principle of equivalence
equation
-
fiber product, pullback
-
homotopy pullback
-
Examples.
-
linear equation, differential equation, ordinary differential equation, critical locus
-
Euler-Lagrange equation, Einstein equation, wave equation
-
Schrödinger equation, Knizhnik-Zamolodchikov equation, Maurer-Cartan equation, quantum master equation, Euler-Arnold equation, Fuchsian equation, Fokker-Planck equation, Lax equation
Contents
Definition
Given a set , the identity function on is the function that maps any element of to itself:
or equivalently,
Thus, the identity function is the function for which every element of is a fixed point.
The identity functions are the identity morphisms in the category Set of sets.
More generally, in any concrete category, the identity morphism of each object is given by the identity function on its underlying set.
Definition
In (dependent) type theory, the identity function on a type may be declared as
(1)
Properties
Definition
In dependent type theory, the type of identity functions on a type is the type
of functions with a witness that every element is a fixed point of the function.
In general, an identity function is an element of this type. However, any element of the type of identity functions is unique up to identification:
Theorem
For all types , the type
is a proposition.
Proof
Suppose we have with and with . Then we have a homotopy
and by function extensionality, an identification
and by dependent function application on this identification, a dependent identification
Then by the extensionality principle for dependent pair types, we have
in the identity type
By induction on dependent pair types, this implies that for all elements
Thus, the type
is a proposition.
Theorem
For all types , the type
is contractible.
Proof
Since the type
is a proposition, it suffices to construct an element of the above type. Given a type , by the weakening rules and the generic variable rule in dependent type theory, one gets the identity family of elements . Then by lambda abstraction, one gets a function , and by the typal computation rule for weak function types one gets the dependent function . For strict function types, we have . Thus, one has the identity function
Since the type
is a proposition and has element , the type is contractible.
Thus, it makes sense to refer to the canonical identity function as the identity function on type .
Now, we show that the identity function is an equivalence of types:
Theorem
Any identity function is a (non-coherent) involution.
Proof
Given a function and a dependent function , by function application on , we have the family of identifications
Thus by concatenation of identifications and lambda abstraction, we have the dependent function
which indicates that the identity function is a non-coherent involution.
By definition of involution, it follows that:
Corollary
The inverse function of the identity function is the identity function itself.
Theorem
Any identity function is bi-invertible.
Proof
Given a function and a dependent function , we have an element
of type
indicating that is bi-invertible.
By definition, it follows that:
Hence, in dependent type theory, the identity function is also called the identity equivalence.
There are other ways to prove that the identity function is an equivalence of types. One of them is given below:
Proof
The fiber type in question is the dependent type
By the judgmental computation rule of function types, the term reduces down to , and the fiber type becomes
This is always a contractible type:
By induction on dependent sum types, it suffices to construct an identification
for any and , and by induction on identity types, it suffices to construct an identification
but that’s just reflexivity on
Thus, for all , the fiber type of the identity function at is contractible.