Solution (source code)

= Solution

For $D:\mathcal I\to\mathcal C$, define the <functor> $\operatorname{Cone}(-,D):\mathcal C^{\mathrm{op}}\to\mathbf{Set}$ by
$$
\operatorname{Cone}(X,D)=\operatorname{Nat}(\Delta X,D),
$$
where $\Delta X$ is the <constant diagram functor>; a <morphism> into $X$ acts by precomposition on every <categorical cone> leg. A <categorical limit> is a <representation of a functor> of the form
$$
\boxed{\mathcal C(-,L)\cong\operatorname{Cone}(-,D).}
$$
The image of $1_L$ is the universal <categorical cone> $\lambda:\Delta L\to D$. By <naturality> of the representing <isomorphism>, the image of $h:X\to L$ is $\lambda\circ\Delta h$. Thus this definition is exactly existence and uniqueness of factorization of every <categorical cone> through $\lambda$. Conversely that <universal property> gives the representing <natural bijection>.