In category theory it can be proven that the identity function is unique. It is also said that, reasoning with parametricity, that the type `forall a. a -> a` has only one inhabitant. In Haskell though I can think of more implementations of the identity function:

```
id x = x
id x = fst (x, "useless")
id x = head [x]
id x = (\x -> x) x
id x = (\x -> (\x -> x) x) x

```

How can I understand the statement "the identity function is unique" and "any function with type `forall a. a -> a` has only one inhabitant" when there are multiple implementations?