Michael Shulman closed category

In the definition of closed category, the hom-sets $C(X,Y)$ for $X\neq I$ are redundant information, being isomorphic to $C(I,[X,Y])$. If we remove them, we obtain an axiomatization of a closed category that doesn’t assume from the outset that we are given a category at all.

I will use the Eilenberg-Kelly notion of closed category, with a given “underlying-set functor” $U:C\to Set$ such that $U([X,Y]) = C(X,Y)$ (and another axiom); this enables us to simply replace $C(X,Y)$ everywhere that it appears by $U([X,Y])$. I will also make two notational changes, writing $X\Rightarrow Y$ instead of $[X,Y]$, and writing $x \Vdash X$ instead of $x\in U(X)$.

The data we are given is now the following. We start with the following stuff:

• A set of objects $X,Y,Z,\dots$.
• For any two objects $X,Y$, an object $X\Rightarrow Y$.
• An object $I$.
• For any object $X$, a set of “realizers” denoted $x\Vdash X$.

Add the following structure:

• For any $f\Vdash X\Rightarrow Y$ and $g:Y\Rightarrow Z$ a composite $g\circ f \Vdash X\Rightarrow Z$ (composition in the category $C$).
• For any $X$ a realizer $1_X \Vdash X\Rightarrow X$ (identities in the category $C$).
• For any $f\Vdash X' \Rightarrow X$ and $g\Vdash Y \Rightarrow Y'$, a realizer $(f\Rightarrow g) \Vdash (X\Rightarrow Y) \Rightarrow (X' \Rightarrow Y')$ (functoriality of $[-,-]$).
• For any $f\Vdash X\Rightarrow Y$ and $x\Vdash X$, a realizer $f\cdot x \Vdash Y$ (functoriality of $U$).
• For any $X$, realizers $i_X \Vdash X \Rightarrow (I \Rightarrow X)$ and $i'_X \Vdash (I\Rightarrow X) \Rightarrow X$.
• For any $X$, a realizer $j_X \Vdash I \Rightarrow (X\Rightarrow X)$.
• For any $X,Y,Z$, a realizer $L^X_{Y Z} \Vdash (Y\Rightarrow Z) \Rightarrow ((X\Rightarrow Y) \Rightarrow (X \Rightarrow Z))$.

And impose the following axioms:

• $h\circ (g\circ f) = (h\circ g)\circ f$
• $f \circ 1_X = f = 1_Y \circ f$
• $(1_X \Rightarrow 1_Y) = 1_{X\Rightarrow Y}$
• $(h \Rightarrow k) \circ (f\Rightarrow g) = (h \circ f) \Rightarrow (g\circ k)$
• $1_X \cdot x = x$
• $(g\circ f) \cdot x = g \cdot (f\cdot x)$
• $(h \Rightarrow f) \cdot g = f\circ g\circ h$
• $i'_X \circ i_X = 1_X$ and $i'_X \circ i_X = 1_{I\Rightarrow X}$
• $i_Y \circ f = (1_I \Rightarrow f) \circ i_X$ and (redundantly) $i'_Y \circ (1_I \Rightarrow f) = f \circ i'_X$
• $(1_X \Rightarrow f) \circ j_X = (f\Rightarrow 1_Y) \circ j_Y$
• $(1_{Y\Rightarrow Z} \Rightarrow ((1_X \Rightarrow f) \Rightarrow (1_X \Rightarrow g))) \circ L^X_{Y Z} = L^X_{Y' Z'} \circ (f\Rightarrow g)$
• $((h \Rightarrow 1_Y) \Rightarrow 1_{X\Rightarrow Z}) \circ L^X_{Y Z} = (1_{X'\Rightarrow Y} \Rightarrow (h \Rightarrow 1_Z)) \circ L^{X'}_{Y Z}$
• $L^X_{Y Y} \circ j_Y = j_{X\Rightarrow Y}$
• $(j_X \Rightarrow 1_{X\Rightarrow Y}) \circ L^X_{X Y} = i_{X\Rightarrow Y}$
• $(i_Y \Rightarrow 1_{I\Rightarrow Z}) \circ L^I_{Y Z} = (1_{Y} \Rightarrow i_Z)$
• $(1_{Y\Rightarrow U} \Rightarrow L^X_{Y V}) \circ L^Y_{U V} = (L^X_{Y U} \Rightarrow 1_{(X\Rightarrow Y)\Rightarrow (X \Rightarrow V)}) \circ L^{X\Rightarrow Y}_{(X\Rightarrow U),(X\Rightarrow V)} \circ L^X_{U V}$
• $i_{X\Rightarrow X} \cdot 1_X = j_X$.

However, this definition still contains redundant data. The most obvious is $j_X$, which by the last axiom could be simply defined to be $i_{X\Rightarrow X} \cdot 1_X$. This was already noted by Eilenberg-Kelly, who also asserted that $j$ thusly defined is automatically natural (i.e. the axiom $(1_X \Rightarrow f) \circ j_X = (f\Rightarrow 1_Y) \circ j_Y$ is redundant). To see this, first note that Lemma 2.2 of EK says that for $f \Vdash (A\Rightarrow A)\Rightarrow X$ we have (using naturality of $i$):

$$i_A \cdot (f\cdot 1_A) = (i_A \circ f) \cdot 1_A = ((1_I \Rightarrow f) \circ i_{A\Rightarrow A}) \cdot 1_A = (1_I \Rightarrow f) \cdot (i_{A\Rightarrow A} \cdot 1_A) = (1_I \Rightarrow f) \cdot j_A = f\circ j_A.$$

Now Proposition 2.4 says for any $g\Vdash A\Rightarrow B$ we have (applying 2.2 with $f = (1_A \Rightarrow g)$ and $(g \Rightarrow 1_B)$ respectively, and using the axiom $(h \Rightarrow f) \cdot g = f\circ g\circ h$):

$$(1_A \Rightarrow g) \circ j_A = i_A \cdot ((1_A \Rightarrow g)\cdot 1_A) = i_A \cdot g$$

$$(g \Rightarrow 1_B) \circ j_A = i_A \cdot ((g \Rightarrow 1_B) \cdot 1_A) = i_A \circ g$$

so that $(1_A \Rightarrow g) \circ j_A = (g \Rightarrow 1_B) \circ j_A$, i.e. $j$ is natural (which we did not use in this proof).

We note the other basic propositions of EK in our notation. Prop 2.5 says $i_{I\Rightarrow A} = (1_I \Rightarrow i_A)$, since when precomposed with the isomorphism $i_A$ they are equal by naturality. Prop 2.6 says for $f\Vdash I\Rightarrow A$ we have $i_A \circ f = i_{I\Rightarrow A} \cdot f$, by acting on $f$ with Prop 2.5. Taking $A=I$ and $f=1$ then gives Prop 2.7: $j_I = i_I$. In particular, $j_I$ is an isomorphism, so putting $X=Y$ in its naturality we get Prop 2.8: $(1_I \Rightarrow f) = (f\Rightarrow 1_I)$ for any $f\Vdash I \Rightarrow I$. By acting on $g\Vdash I\Rightarrow I$ this gives Prop 2.9: $f\circ g = g\circ f$, i.e. the monoid of endomorphisms of $I$ is commutative.

The next most obvious redundancy is that the axiom $(h \Rightarrow f) \cdot g = f\circ g\circ h$ says that composition can be defined in terms of the “functorial” action of $\Rightarrow$ and the “action” $\cdot$. However, using this axiom to define binary composition would involve a seemingly-arbitrary choice of which of $f,g,h$ to take as an identity. A better option is to note that by Proposition 2.3 in Eilenberg-Kelly, the axiom $L^X_{Y Y} \circ j_Y = j_{X\Rightarrow Y}$ is equivalent to

• $L^X_{Y Z} \cdot f = (1_X \Rightarrow f)$ for any $f\Vdash Y\Rightarrow Z$.

and therefore we also have

$$(L^X_{Y Z} \cdot f) \cdot g = (1_X \Rightarrow f) \cdot g = f\circ g \circ 1_X = f\circ g$$

for any $f\Vdash Y\Rightarrow Z$ and $g\Vdash X \Rightarrow Y$. Thus, the natural definition of $f\circ g$ is as $(L^X_{Y Z} \cdot f) \cdot g$.

I expect, with this definition, that it should be possible to prove associativity and unitality of composition, and naturality of $i$, from the corresponding “internalized” properties for $L^X_{Y Z}$.

We may be able to define $(f\Rightarrow g)$ in terms of the other data; we have already noted that $(1\Rightarrow f)$ is definable, so all that remains to define is $(f\Rightarrow 1)$. In the symmetric case, there is no problem; in the non-symmetric case we argue that $(f\Rightarrow 1) = L^X_{Y Z} \circ ev_f = (L^{(X\to Y)\to (X\to Z)}_{(Y\to Z),(X\to Z)} \cdot ev_f) \cdot L^X_{Y Z}$.