Skip to content

Instantly share code, notes, and snippets.

Last active Jun 25, 2017
What would you like to do?
Identity function, id :: a -> a

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 (identity expansion for terminals) If T is a terminal object then !(T) = id(T).

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

Lemma (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 (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 (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)

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented May 29, 2017

I have many examples of usefulness of id here.


This comment has been minimized.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment