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 ≔ Tin the definition.
Lemma 18.104.22.168 (identity expansion for terminals) If
Tis a terminal object then
!(T) = id(T).
Lemma 22.214.171.124 (identity expansion for initials) If
Sis an initial object then
¡(S) = id(S).
Lemma 126.96.36.199 (identity expansion for products) If
Pis a product of
⟨𝑝0, 𝑝1⟩ = id(P).
fst @a @b &&& snd @a @b = id @(a, b)
Lemma 188.8.131.52 (identity expansion for coproducts) If
Qis a coproduct of
[𝑞0, 𝑞1] = id(Q).
Left @a ||| Right @b = id @(Either a b)
Lemma 184.108.40.206 (identity expansion for exponentials) If
Eis an exponential of
λ(ε) = id(E).
curry @(b -> c) @b @c (\(f, x) -> f x) = id @(b -> c)