# 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

It has to satisfy the properties of the identity arrow - i.e. its left and right composition with any other arrow is that arrow.

Of course, you can have multiple different categories where the objects are types (for some definition of "types" - it's actually really complicated, if not impossible, once you start looking at polymorphic or dependent types) and arrows are something somehow related to functions between them. What exactly you choose to call "arrow" is up to you, as long as it satisfies the required properties (composition and identity).

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.

• Need to think about it, but I'm using Hask (the idealized category of Haskell programs where objects are types and arrows are functions) – GClaramunt Oct 7 '14 at 19:48