Let $$ be a biCartesian closed category. In fact, say $ = \textbf{Set}$, for simplicity. Denote the internal home functor $[A, B] = \hom(A, B)$. If I have a pair $[B, C] × [A, B]$, it feels to me like I should be able to compose universal arrows to get $[A, C] = [B, C] ∘ [A, B]$, if you'll excuse the abuse of notation (the ring operator).
It must admit a simple and elegant solution. I have something (slightly half-baked) and I was wondering if anyone could lend some insight to either find another direction or finish it off.
My (modest) start
Let $ε$ be the evaluation morphism. I'm trying to define a universal arrow as an infix operator $[B, C] ⋄ [A, B]$. It has the property that it makes the following diagram commute:
$\require{AMScd}$ \begin{CD} [B, C] × [A, B] @>{∃!\ (⋄)}>> [A, C] \\ \\ [A, C] × A @>{ε}>> C\\ @A{(⋄) × \mathrm{id}}AA @|\\ [B, C] × [A, B] × A @>>{ε ∘ (\mathrm{id} × ε)}> C \end{CD}
I'm not exactly sure how to prove the existence or uniqueness (up to $≅$), but I think along these lines:
- Existence is down to the fact that $\hom(X, Y) ≅ [X, Y]$ for all $X, Y ∈ $. So if $A \xrightarrow{g ∘ f} C$ exists in $\hom(A, C)$ (which it must axiomatically) then $[B, C] ⋄ [A, B]$ it exists in $[A, C]$. The formalities would have to abstract through diagrams of global elements $1 \xrightarrow{f} [A, B]$ and $1 \xrightarrow{g} [B, C]$ and their interoperation with $ε$.
- Uniqueness, I'm not sure where to start. Maybe I could use the adjunctions ${-} ⊗ X ⊣ [X, {-}]$ which give me isomorphism to show uniqueness up to isomorphism?
$\require{AMScd}\newcommand{\C}{\mathscr{C}}\newcommand{\hom}{\operatorname{hom}}\newcommand{\id}{\mathrm{id}}$Forget about coproducts, we want only a category $\C$ with all finite products and all exponential objects. Your initial question about existence is unclear to me, since the diagram you drew defines a unique such arrow $\diamond$ by basic adjunction properties (you're going to kick yourself).
Instead, I'll add a little bit more about this definition of composition arrow (which I'll denote $\circ$). There is some sense in which $\circ$ is the composition arrow for the category $\C$, if one wants to enter into enriched category theory.
Our category is canonically a symmetric closed monoidal category $(\C,\times,\hom;\alpha,\lambda,\rho,\gamma)$ where $\times:\C\times\C\to\C$ is a choice of Cartesian product functor and $\alpha:(-)\times((-)\times(-))\cong((-)\times(-))\times(-)$, $\lambda:1\times(-)\cong(-)$, $\rho:(-)\times1\cong(-)$ are the canonical natural isomorphisms and $\gamma$ is the canonical symmetry $a\times b\cong b\times a$, natural in both variables.
So, $\C$ is a base of enrichment. It is well known that any base of enrichment is canonically enriched over itself; in particular, composition morphisms exist in a sensible way.
Fix $x,y,z\in\C$. Define: $$\circ:\hom(y,z)\times\hom(x,y)\to\hom(x,z)$$As the $-\times x\dashv\hom(x,-)$ adjunct of the arrow: $$(\hom(y,z)\times\hom(x,y))\times x\overset{\alpha}{\longrightarrow}\hom(y,z)\times(\hom(x,y)\times x)\overset{1\times\epsilon}{\longrightarrow}\hom(y,z)\times y\overset{\epsilon}{\longrightarrow}z$$
It can be shown that the arrows $\circ$ so defined satisfy the following properties:
$$\begin{CD}\hom(y,z)\times(\hom(x,y)\times\hom(w,x))@>1\times\circ>>\hom(y,z)\times\hom(w,y)\\@V\alpha VV@VV1V\\(\hom(y,z)\times\hom(x,z))\times\hom(w,x)@.\hom(y,z)\times\hom(w,y)\\@V\circ\times1VV@VV\circ V\\\hom(x,z)\times\hom(w,x)@>>\circ>\hom(w,z)\end{CD}$$
$$\begin{CD}\hom(x,y)@<\rho<<\hom(x,y)\times1\\@V1VV@VV1\times\id_x V\\\hom(x,y)@<<\circ<\hom(x,y)\times\hom(x,x)\end{CD}$$
$$\begin{CD}\hom(x,y)@<\lambda<<1\times\hom(x,y)\\@V1VV@VV\id_y\times1 V\\\hom(x,y)@<<\circ<\hom(y,y)\times\hom(x,y)\end{CD}$$
And further that if $f:x\to y$ then if $f$ is identified with its sister arrow $1\to\hom(x,y)$ we have: $$\hom(1,f):\hom(a,x)\to\hom(a,y)\\=\\\hom(a,x)\overset{\lambda^{-1}}{\cong}1\times\hom(a,x)\overset{f\times1}{\longrightarrow}\hom(x,y)\times\hom(a,x)\overset{\circ}{\longrightarrow}\hom(a,y)$$A similar results holds for $\hom(f,1)$ if and only if we assume that the given adjunction $\kappa:\C(x\times y,z)\cong\C(x,\hom(y,z))$ is natural in all variables.
So yes, this arrow $\circ$ or $\diamond$ (trivially ?) exists and it satisfies some quite nice general properties.
As for uniqueness of an arrow $\circ$ making all those diagrams commute (this is not your original question of uniqueness, that follows immediately) that's sort-of true but as far as I know it's not literally true.
By sort-of true I mean there is a subtle necessary and sufficient condition involving enriched natural transformations which you probably don't care about. If asked, I will write this up.