nLab identity function

Redirected from "type of identity functions".
Contents

Contents

Definition

Given a set SS, the identity function on SS is the function id S:SSid_S\colon S \to S that maps any element xx of SS to itself:

id S=(xx)=λx.x; id_S = (x \mapsto x) = \lambda x.\; x ;

or equivalently,

id S(x)=x. id_S(x) = x .

Thus, the identity function is the function for which every element xx of SS 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 TT may be declared as

(1)id T(λ(t:T).t):TT. \mathrm{id}_T \;\coloneqq\; \big(\lambda(t \colon T).t \big) \;\colon\; T \to T \,.

 Properties

Definition

In dependent type theory, the type of identity functions on a type AA is the type

f:AA x:Af(x)= Ax\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

of functions with a witness that every element x:Ax: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:

Theorem

For all types AA, the type

f:AA x:Af(x)= Ax\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

is a proposition.

Proof

Suppose we have i:AAi:A \to A with I: x:Ai(x)= AxI:\prod_{x:A} i(x) =_A x and j:AAj:A \to A with J: x:Aj(x)= AxJ:\prod_{x:A} j(x) =_A x. Then we have a homotopy

λx:A.I(x)J(x) 1: x:Ai(x)= Aj(x)\lambda x:A.I(x) \bullet J(x)^{-1}:\prod_{x:A} i(x) =_A j(x)

and by function extensionality, an identification

homToId(i,j,λx:A.I(x)J(x) 1):i= AAj\mathrm{homToId}(i, j, \lambda x:A.I(x) \bullet J(x)^{-1}):i =_{A \to A} j

and by dependent function application on this identification, a dependent identification

apd(i,j,homToId(i,j,λx:A.I(x)J(x) 1,I,J):I= f:AA. x:Af(x)= Aj(x) i,j,λx:A.I(x)J(x) 1J\mathrm{apd}(i, j, \mathrm{homToId}(i, j, \lambda x:A.I(x) \bullet J(x)^{-1}, I, J):I =_{f:A \to A.\prod_{x:A} f(x) =_A j(x)}^{i, j, \lambda x:A.I(x) \bullet J(x)^{-1}} J

Then by the extensionality principle for dependent pair types, we have

pairIdsToId(i,j,I,J)(homToId(i,j,λx:A.I(x)J(x) 1),apd(i,j,homToId(i,j,λx:A.I(x)J(x) 1,I,J))\mathrm{pairIdsToId}(i, j, I, J)(\mathrm{homToId}(i, j, \lambda x:A.I(x) \bullet J(x)^{-1}), \mathrm{apd}(i, j, \mathrm{homToId}(i, j, \lambda x:A.I(x) \bullet J(x)^{-1}, I, J))

in the identity type

(i,I)= f:AA x:Af(x)= Ax(j,J)(i, I) =_{\sum_{f:A \to A} \prod_{x:A} f(x) =_A x} (j, J)

By induction on dependent pair types, this implies that for all elements

F: f:AA x:Af(x)= AxandG: f:AA x:Af(x)= Ax,F:\sum_{f:A \to A} \prod_{x:A} f(x) =_A x \; \mathrm{and} \; G:\sum_{f:A \to A} \prod_{x:A} f(x) =_A x \; ,
F= f:AA x:Af(x)= AxGF =_{\sum_{f:A \to A} \prod_{x:A} f(x) =_A x} G

Thus, the type

f:AA x:Af(x)= Ax\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

is a proposition.

Theorem

For all types AA, the type

f:AA x:Af(x)= Ax\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

is contractible.

Proof

Since the type

f:AA x:Af(x)= Ax\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

is a proposition, it suffices to construct an element of the above type. Given a type AA, by the weakening rules and the generic variable rule in dependent type theory, one gets the identity family of elements x:Ax:Ax:A \vdash x:A. Then by lambda abstraction, one gets a function λx:A.x:AA\lambda x:A.x:A \to A, and by the typal computation rule for weak function types one gets the dependent function β AA x:A.x: x:A(λx:A.x)(x)= Ax\beta_{A \to A}^{x:A.x}:\prod_{x:A} (\lambda x:A.x)(x) =_A x. For strict function types, we have β AA x:A.xrefl A\beta_{A \to A}^{x:A.x} \equiv \mathrm{refl}_A. Thus, one has the identity function

(λx:A.x,β AA x:A.x): f:AA x:Af(x)= Ax(\lambda x:A.x, \beta_{A \to A}^{x:A.x}):\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

Since the type

f:AA x:Af(x)= Ax\sum_{f:A \to A} \prod_{x:A} f(x) =_A x

is a proposition and has element (λx:A.x,β AA x:A.x)(\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 λx:A.x\lambda x:A.x as the identity function on type AA.

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 i:AAi:A \to A and a dependent function I: x:Ai(x)= AxI:\prod_{x:A} i(x) =_A x, by function application on ii, we have the family of identifications

x:Aap(i,i(x),x,I(x)):i(i(x))= Ai(x)x:A \vdash \mathrm{ap}(i, i(x), x, I(x)):i(i(x)) =_A i(x)

Thus by concatenation of identifications and lambda abstraction, we have the dependent function

λx:A.ap(i,i(x),x,I(x))I(x): x:Ai(i(x))= Ax\lambda x:A.\mathrm{ap}(i, i(x), x, I(x)) \bullet I(x):\prod_{x:A} i(i(x)) =_A x

which indicates that the identity function i:AAi:A \to A 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 i:AAi:A \to A and a dependent function I: x:Ai(x)= AxI:\prod_{x:A} i(x) =_A x, we have an element

((i,λx:A.ap(i,i(x),x,I(x))I(x)),(i,λx:A.ap(i,i(x),x,I(x))I(x)))((i, \lambda x:A.\mathrm{ap}(i, i(x), x, I(x)) \bullet I(x)), (i, \lambda x:A.\mathrm{ap}(i, i(x), x, I(x)) \bullet I(x)))

of type

( j:AA x:Ai(j(x))= Ax)×( k:AA x:Ak(i(x))= Ax)\left(\sum_{j:A \to A} \prod_{x:A} i(j(x)) =_A x\right) \times \left(\sum_{k:A \to A} \prod_{x:A} k(i(x)) =_A x\right)

indicating that i:AAi:A \to A is bi-invertible.

By definition, it follows that:

Corollary

Any identity function on a type AA 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:

Theorem

Suppose that function types are defined using judgmental computation rules. Then for all terms x:Tx \colon T, the fiber of the identity function λ(t:T).t:TT\lambda(t \colon T).t \,\colon\, T \to T (1) at xx is a contractible type.

Proof

The fiber type in question is the dependent type

y:T(λ(t:T).t)(y)= Tx. \sum_{y \colon T} \big( \lambda(t:T).t \big)(y) =_T x \,.

By the judgmental computation rule of function types, the term (λ(t:T).t)(x)\big(\lambda(t:T).t\big)(x) reduces down to xx, and the fiber type becomes

y:Ty= Tx \sum_{y \colon T} y \;=_T\; x

This is always a contractible type:

z= y:Ty= Tx(x,refl T(x)). z \;=_{\sum_{y:T} y =_T x}\; \big( x, \mathrm{refl}_T(x) \big) \,.

By induction on dependent sum types, it suffices to construct an identification

(w,p)= y:Ty= Tx(x,refl T(x)) (w, p) \;=_{\sum_{y:T} y =_T x}\; \big( x, \mathrm{refl}_T(x) \big)

for any w:Tw \colon T and p:w= Txp \;\colon\; w =_T x, and by induction on identity types, it suffices to construct an identification

(x,refl T(x))= y:Ty= Tx(x,refl T(x)) \big(x, \mathrm{refl}_T(x)\big) \;=_{\sum_{y:T} y =_T x}\; \big(x, \mathrm{refl}_T(x)\big)

but that’s just reflexivity on (x,refl T(x))(x, \mathrm{refl}_T(x))

refl y:Ty= Tx((x,refl T(x))):(x,refl T(x))= y:Ty= Tx(x,refl T(x)). \mathrm{refl}_{\sum_{y:T} y =_T x} \big( (x, \mathrm{refl}_T(x)) \big) \;\colon\; \big(x, \mathrm{refl}_T(x)\big) \;=_{\sum_{y:T} y =_T x}\; \big(x, \mathrm{refl}_T(x)\big) \,.

Thus, for all x:Tx \colon T, the fiber type of the identity function λ(t:T).t:TT\lambda(t:T).t:T \to T at xx 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.