Closed Category

A closed category is like a Closed Monoidal Category, but without the monoidal structure. Rather than axiomatizing the monoidal structure and asking for a right adjoint to $A\otimes-$, we instead axiomatize the properties of the Internal Hom directly.

Explicitly, a category $V$ is closed if it is equipped with the following data:

• A Profunctor $[-,=]:V^{\mathrm{op}}\times V\to\mathrm{Sets}$
• A unit $I:V$
• A natural isomorphism $i:\mathrm{Id}\cong[I,-]$
• An Extranatural Transformation $\iota:I\to[X,X]$, extranatural in $X$.
• An Extranatural Transformation $c:[Y,Z]\to[[X,Y],[X,Z]]$, natural in $Y$ and $Z$ and extranatural in $X$.

Such that the following diagrams commute:

• Left identity:

• Right identity:

• Associativity:

• Externalisation: The map $V(X,Y)\to V(I,[X,Y])$ defined by $f\mapsto[id,f]\circ\iota_{X}$ is an Equivalence.

Via Display

The original Eilenberg-Kelly definition of a closed category used an underlying set functor $U:V\to\mathrm{Sets}$ with a condition that $U\circ[-,=]=V(-,=)$ Can this be done via display instead?