Closed category

A closed category is a category with objects resembling hom-sets. #m/def/cat Explicitly, a closed category $𝖢$ is equipped with¹²

a multifunctor $[-, -] : 𝖢 𝐨 𝐩 \times 𝖢 \to 𝖢$ called the internal hom-functor;
an object $1$ called the unit;
a natural isomorphism with components $𝜖 𝑋 : 𝑋 \to [1, 𝑋]$ in $𝖢 𝖢$ , which may be thought of as enabling generalized elements;
an extranatural transformation with components $𝜄 𝑋 : 1 \to [𝑋, 𝑋]$ , which may be thought of as the generalized element for the identity;
an (extra)natural transformation with components $𝐿 𝑋 𝑌, 𝑍 : [𝑌, 𝑍] \to [[𝑋, 𝑌], [𝑋, 𝑍]]$ , which may be thought of as encoding composition

such that

commute for any objects $𝑋, 𝑌, 𝑍, 𝑈, 𝑉 \in 𝖢$ , and the map defined by

𝛾 : 𝖢 (𝑋, 𝑌) \to 𝖢 (1, [𝑋, 𝑌]) 𝑓 \mapsto [i d 𝑋, 𝑓] (𝜄 𝑋)

Archetypal example:

𝖲 𝖾 𝗍

In $𝖲 𝖾 𝗍$ the internal hom-functor is the ordinary Hom-functor

(- \to -) = [-, -] = 𝖲 𝖾 𝗍 : 𝖲 𝖾 𝗍 𝐨 𝐩 \times 𝖲 𝖾 𝗍 \to 𝖲 𝖾 𝗍

and the unit $1$ is any singleton. Then the (extra)natural transformations are given by

𝜖 𝑋 : 𝑋 \to (1 \to 𝑋) 𝑥 \mapsto (1 \mapsto 𝑥)

and

𝜄 𝑋 : 1 \to (𝑋 \to 𝑋) 1 \mapsto 1 𝑋

and

𝐿 𝑋 𝑌, 𝑍 : (𝑌 \to 𝑍) \to ((𝑋 \to 𝑌) \to (𝑋 \to 𝑍)) 𝑓 \mapsto (𝑔 \mapsto 𝑓 \circ 𝑔)

A Closed monoidal category is a category which is also monoidal in a compatible way.

#state/tidy | #lang/en | #SemBr

1966. Closed categories, §I.2, pp. 428–430. Note the refined definition uses only CC1–4 ↩
1977. Embedding of Closed Categories Into Monoidal Closed Categories, §1, p. 86. Refines the original definition with CC5, which guarantees the bijection $𝛾$ ↩

Footnotes