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 a set $S$, the identity function on $S$ is the function $id_S\colon S \to S$ that maps any element $x$ of $S$ to itself:
or equivalently,
Thus, the identity function is the function for which every element $x$ of $S$ 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.
In (dependent) type theory, the identity function on a type $T$ may be declared as
In dependent type theory, the type of identity functions on a type $A$ is the type
of functions with a witness that every element $x:A$ 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:
For all types $A$, the type
is a proposition.
Suppose we have $i:A \to A$ with $I:\prod_{x:A} i(x) =_A x$ and $j:A \to A$ with $J:\prod_{x:A} j(x) =_A x$. 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.
For all types $A$, the type
is contractible.
Since the type
is a proposition, it suffices to construct an element of the above type. Given a type $A$, by the weakening rules and the generic variable rule in dependent type theory, one gets the identity family of elements $x:A \vdash x:A$. Then by lambda abstraction, one gets a function $\lambda x:A.x:A \to A$, and by the typal computation rule for weak function types one gets the dependent function $\beta_{A \to A}^{x:A.x}:\prod_{x:A} (\lambda x:A.x)(x) =_A x$. For strict function types, we have $\beta_{A \to A}^{x:A.x} \equiv \mathrm{refl}_A$. Thus, one has the identity function
Since the type
is a proposition and has element $(\lambda x:A.x, \beta_{A \to A}^{x:A.x})$, the type is contractible.
Thus, it makes sense to refer to the canonical identity function $\lambda x:A.x$ as the identity function on type $A$.
Now, we show that the identity function is an equivalence of types:
Any identity function is a (non-coherent) involution.
Given a function $i:A \to A$ and a dependent function $I:\prod_{x:A} i(x) =_A x$, by function application on $i$, 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 $i:A \to A$ is a non-coherent involution.
By definition of involution, it follows that:
The inverse function of the identity function is the identity function itself.
Any identity function is bi-invertible.
Given a function $i:A \to A$ and a dependent function $I:\prod_{x:A} i(x) =_A x$, we have an element
of type
indicating that $i:A \to A$ is bi-invertible.
By definition, it follows that:
Any identity function on a type $A$ is an equivalence of types.
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:
Suppose that function types are defined using judgmental computation rules. Then for all terms $x \colon T$, the fiber of the identity function $\lambda(t \colon T).t \,\colon\, T \to T$ (1) at $x$ is a contractible type.
The fiber type in question is the dependent type
By the judgmental computation rule of function types, the term $\big(\lambda(t:T).t\big)(x)$ reduces down to $x$, and the fiber type becomes
This is always a contractible type:
the center of contraction is given by the dependent pair $(x, \mathrm{refl}_T(x))$,
for any $z \colon \sum_{y \colon T} y \,=_T\, x$, there is an identification
By induction on dependent sum types, it suffices to construct an identification
for any $w \colon T$ and $p \;\colon\; w =_T x$, and by induction on identity types, it suffices to construct an identification
but that’s just reflexivity on $(x, \mathrm{refl}_T(x))$
Thus, for all $x \colon T$, the fiber type of the identity function $\lambda(t:T).t:T \to T$ at $x$ is contractible.
Last revised on November 4, 2023 at 23:01:09. See the history of this page for a list of all contributions to it.