Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Last active Jun 25, 2017
Embed
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 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)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented May 29, 2017

I have many examples of usefulness of id here.

@Icelandjack

This comment has been minimized.

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