{{ message }}

Instantly share code, notes, and snippets.

# Icelandjack/id.markdown

Last active Jun 25, 2017
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 commented May 29, 2017

 I have many examples of usefulness of `id` here.