# Identity in the category of types and functions

In the model of (functional) programming languages as a category where the objects are types and the arrows are functions, I'm trying to really understand what's really the identity arrow.

Barr-Wells "Category Theory for CS" says you need the id function, but I wonder: it really has to be the "do nothing" function? For any type A, doesn't any function f:A->A work? If looking at type level, I can't distinguish the functions, shouldn't be ok?

I'm trying to find a counter-example but couldn't.

EDIT: I was thinking on the Hask category but I guess my question in Category Theory terms is: Does every endomorphism in an object A is isomorphic to the identity arrow in A?

• What do you mean? You can't identify a function by it's type. f: int -> int can be the ID function, but can also be increment by 1 function. – Roi Divon Oct 6 '14 at 14:50
• Yeah, that's my point :) – GClaramunt Oct 7 '14 at 14:16
• Maybe is a question for Mathematics stackexchange – GClaramunt Oct 10 '14 at 14:26

A trivial example, you can say that "let us define that the (sole) arrow between type $A$ and type $B$ represents the family of all functions between $A$ and $B$" - in this category the sole arrow $A \to A$ will happen to also be the identity arrow. I suppose this is what you mean under "looking at type level".
Or you can say: For a given family of equivalence relations $Eq_T$ on every type $T$, let us define that there is one arrow between type $A$ and type $B$ for every function $A \to B$, modulo the function equivalence relation "maps $Eq_A$ to $Eq_B$". Then if you take the usual equality relation on integers and consider the arrows $int \to int$, in this category you'll only have one identity arrow - the function that maps a number to itself. The function $x \to x+1$ will not work.