[proofplan] The hypothesis says precisely that each morphism from $c$ into an object of $\mathcal A$ factors uniquely through $\eta_c: c \to I(L(c))$. We use this universal property to define $L$ on morphisms: a morphism $u: c \to d$ is sent to the unique map $L(u): L(c) \to L(d)$ corresponding to $\eta_d \circ u$. The same uniqueness proves that identities and compositions are preserved. Finally, the universal factorization gives the adjunction bijections, and direct computations verify their naturality. [/proofplan] [step:Define the action of $L$ on morphisms by the universal property] Let $u: c \to d$ be a morphism in $\mathcal C$. Apply the assumed universal property for the object $c \in \mathcal C$, the object $L(d) \in \mathcal A$, and the morphism \begin{align*} \eta_d \circ u: c \to I(L(d)) \end{align*} in $\mathcal C$. There exists a unique morphism \begin{align*} L(u): L(c) \to L(d) \end{align*} in $\mathcal A$ such that \begin{align*} I(L(u)) \circ \eta_c = \eta_d \circ u. \end{align*} This defines the morphism part of the proposed functor $L: \mathcal C \to \mathcal A$. [guided] We already have an object assignment $c \mapsto L(c)$. To make it into a functor, we must define what happens to a morphism $u: c \to d$ in $\mathcal C$. The target should be a morphism \begin{align*} L(u): L(c) \to L(d) \end{align*} in $\mathcal A$. The only available tool is the universal property of $\eta_c: c \to I(L(c))$. That universal property classifies morphisms from $c$ into objects of the form $I(a)$, where $a \in \mathcal A$. Here we choose $a = L(d)$. Since $L(d)$ is an object of $\mathcal A$, the morphism \begin{align*} \eta_d \circ u: c \to I(L(d)) \end{align*} is exactly the kind of morphism to which the universal property applies. Therefore there is a unique morphism $L(u): L(c) \to L(d)$ in $\mathcal A$ satisfying \begin{align*} I(L(u)) \circ \eta_c = \eta_d \circ u. \end{align*} This equation is the defining equation for $L(u)$. [/guided] [/step] [step:Verify that $L$ preserves identity morphisms] Let $c \in \mathcal C$. The morphism $\operatorname{id}_{L(c)}: L(c) \to L(c)$ in $\mathcal A$ satisfies \begin{align*} I(\operatorname{id}_{L(c)}) \circ \eta_c = \operatorname{id}_{I(L(c))} \circ \eta_c = \eta_c. \end{align*} By the defining uniqueness for $L(\operatorname{id}_c)$, applied to the morphism $\eta_c \circ \operatorname{id}_c = \eta_c$, we obtain \begin{align*} L(\operatorname{id}_c) = \operatorname{id}_{L(c)}. \end{align*} [/step] [step:Verify that $L$ preserves composition] Let $u: c \to d$ and $v: d \to e$ be morphisms in $\mathcal C$. The composite \begin{align*} L(v) \circ L(u): L(c) \to L(e) \end{align*} is a morphism in $\mathcal A$. Applying $I$ and using functoriality of the inclusion $I$, we compute \begin{align*} I(L(v) \circ L(u)) \circ \eta_c &= I(L(v)) \circ I(L(u)) \circ \eta_c \\ &= I(L(v)) \circ \eta_d \circ u \\ &= \eta_e \circ v \circ u. \end{align*} By definition, $L(v \circ u): L(c) \to L(e)$ is the unique morphism in $\mathcal A$ satisfying \begin{align*} I(L(v \circ u)) \circ \eta_c = \eta_e \circ v \circ u. \end{align*} Hence \begin{align*} L(v \circ u) = L(v) \circ L(u). \end{align*} Thus $L: \mathcal C \to \mathcal A$ is a functor. [guided] To prove functoriality, we must show that the morphism assigned to a composite is the composite of the assigned morphisms. Let \begin{align*} u: c \to d, \qquad v: d \to e \end{align*} be morphisms in $\mathcal C$. The definition of $L(v \circ u)$ says that it is the unique morphism $L(c) \to L(e)$ in $\mathcal A$ whose composite with $\eta_c$ is $\eta_e \circ v \circ u$. Therefore it suffices to prove that $L(v) \circ L(u)$ has this same property. Using the defining equations for $L(u)$ and $L(v)$, we compute \begin{align*} I(L(v) \circ L(u)) \circ \eta_c &= I(L(v)) \circ I(L(u)) \circ \eta_c \\ &= I(L(v)) \circ \eta_d \circ u \\ &= \eta_e \circ v \circ u. \end{align*} The first equality uses that $I$ is a functor. The second equality is the defining property of $L(u)$. The third equality is the defining property of $L(v)$, composed on the right with $u$. Thus $L(v) \circ L(u)$ and $L(v \circ u)$ are two morphisms $L(c) \to L(e)$ in $\mathcal A$ with the same composite after $\eta_c$. The uniqueness clause in the universal property forces them to be equal: \begin{align*} L(v \circ u) = L(v) \circ L(u). \end{align*} [/guided] [/step] [step:Construct the adjunction bijections] For objects $x,y \in \mathcal A$, let $\operatorname{Hom}_{\mathcal A}(x,y)$ denote the set of morphisms from $x$ to $y$ in $\mathcal A$. For objects $x,y \in \mathcal C$, let $\operatorname{Hom}_{\mathcal C}(x,y)$ denote the set of morphisms from $x$ to $y$ in $\mathcal C$. For each object $c \in \mathcal C$ and each object $a \in \mathcal A$, define a map \begin{align*} \Phi_{c,a}: \operatorname{Hom}_{\mathcal A}(L(c), a) &\to \operatorname{Hom}_{\mathcal C}(c, I(a)) \\ g &\mapsto I(g) \circ \eta_c. \end{align*} The assumed universal property says exactly that $\Phi_{c,a}$ is bijective: existence gives surjectivity, and uniqueness gives injectivity. [guided] First define the hom-set notation used in the [adjunction formula](/theorems/3878). For objects $x,y \in \mathcal A$, the symbol $\operatorname{Hom}_{\mathcal A}(x,y)$ denotes the set of morphisms from $x$ to $y$ in $\mathcal A$. For objects $x,y \in \mathcal C$, the symbol $\operatorname{Hom}_{\mathcal C}(x,y)$ denotes the set of morphisms from $x$ to $y$ in $\mathcal C$. The desired adjunction $L \dashv I$ is a natural family of bijections \begin{align*} \operatorname{Hom}_{\mathcal A}(L(c), a) \cong \operatorname{Hom}_{\mathcal C}(c, I(a)). \end{align*} The universal property already provides this bijection. For fixed $c \in \mathcal C$ and $a \in \mathcal A$, define \begin{align*} \Phi_{c,a}: \operatorname{Hom}_{\mathcal A}(L(c), a) &\to \operatorname{Hom}_{\mathcal C}(c, I(a)) \\ g &\mapsto I(g) \circ \eta_c. \end{align*} Surjectivity means that every morphism $f: c \to I(a)$ is equal to $I(g) \circ \eta_c$ for some $g: L(c) \to a$ in $\mathcal A$. This is precisely the existence part of the hypothesis. Injectivity means that if two morphisms $g_1,g_2: L(c) \to a$ satisfy \begin{align*} I(g_1) \circ \eta_c = I(g_2) \circ \eta_c, \end{align*} then $g_1 = g_2$. This is precisely the uniqueness part of the hypothesis, applied to the common morphism $c \to I(a)$. [/guided] [/step] [step:Verify naturality of the adjunction bijections] Let $u: c' \to c$ be a morphism in $\mathcal C$, let $g: L(c) \to a$ be a morphism in $\mathcal A$, and let $h: a \to b$ be a morphism in $\mathcal A$. Naturality in the $\mathcal C$-variable follows from the defining equation for $L(u)$: \begin{align*} \Phi_{c',a}(g \circ L(u)) &= I(g \circ L(u)) \circ \eta_{c'} \\ &= I(g) \circ I(L(u)) \circ \eta_{c'} \\ &= I(g) \circ \eta_c \circ u \\ &= \Phi_{c,a}(g) \circ u. \end{align*} Naturality in the $\mathcal A$-variable follows from functoriality of $I$: \begin{align*} \Phi_{c,b}(h \circ g) &= I(h \circ g) \circ \eta_c \\ &= I(h) \circ I(g) \circ \eta_c \\ &= I(h) \circ \Phi_{c,a}(g). \end{align*} Therefore the bijections $\Phi_{c,a}$ are natural in both variables, so they exhibit $L$ as left adjoint to $I$. [/step] [step:Identify the unit and prove uniqueness of the functor] The naturality identity for $\eta$ is exactly the defining equation for $L(u)$. Indeed, for every morphism $u: c \to d$ in $\mathcal C$, \begin{align*} (I \circ L)(u) \circ \eta_c = I(L(u)) \circ \eta_c = \eta_d \circ u. \end{align*} Hence the family $\eta = (\eta_c)_{c \in \mathcal C}$ is a natural transformation \begin{align*} \eta: \operatorname{id}_{\mathcal C} \Rightarrow I \circ L. \end{align*} Under the adjunction bijection $\Phi_{c,L(c)}$, the morphism $\operatorname{id}_{L(c)}: L(c) \to L(c)$ corresponds to \begin{align*} I(\operatorname{id}_{L(c)}) \circ \eta_c = \eta_c, \end{align*} so $\eta$ is the unit of the adjunction. Finally, suppose $L': \mathcal C \to \mathcal A$ is another functor with the same object assignment $L'(c)=L(c)$ and satisfying \begin{align*} I(L'(u)) \circ \eta_c = \eta_d \circ u \end{align*} for every morphism $u: c \to d$ in $\mathcal C$. For each such $u$, both $L'(u)$ and $L(u)$ are morphisms $L(c) \to L(d)$ in $\mathcal A$ with the same composite after $\eta_c$. By the uniqueness clause in the universal property, $L'(u)=L(u)$. Thus the extension to a functor is unique. [/step]