Identity function, id :: a -> a

id.markdown

Principle of identity expansion

Whenever some construction has a certain relationship to all constructions of the same kind within a category, it must, in particular, have this relationship to itself. Socrates’ dictum to “know thyself” is as important in category theory as it is in life. So whenever we encounter a universal construction we will see what we can learn about it by “probing it with itself”. In the case of a terminal object, this means choosing X ≔ T in the definition.

Lemma 3.1.1.2 (identity expansion for terminals) If T is a terminal object then !(T) = id(T).

Lemma 3.1.4.2 (identity expansion for initials) If S is an initial object then ¡(S) = id(S).

Lemma 3.2.1.2 (identity expansion for products) If P is a product of A and B with projections 𝑝0 and 𝑝1, then ⟨𝑝0, 𝑝1⟩ = id(P).

fst @a @b &&& snd @a @b = id @(a, b)

Lemma 3.3.1.2 (identity expansion for coproducts) If Q is a coproduct of A and B with insertions 𝑞0 and 𝑞1, then [𝑞0, 𝑞1] = id(Q).

Left @a ||| Right @b = id @(Either a b)

Lemma 3.4.1.2 (identity expansion for exponentials) If E is an exponential of A and B then λ(ε) = id(E).

curry @(b -> c) @b @c (\(f, x) -> f x) = id @(b -> c)

I have many examples of usefulness of id here.

https://www.reddit.com/r/haskellquestions/comments/6j3wh7/identity_function/