===== Terminal morphism =====
==== Collection ====
| @#55CCEE: context     | @#55CCEE: $Z:\mathrm{Ob}_{\bf C}$ |
| @#55CCEE: context     | @#55CCEE: $F$ in ${\bf D}\longrightarrow{\bf C}$ |
| @#FFBB00: definiendum | @#FFBB00: $\langle B,\phi\rangle$ in $\mathrm{it}$ |
| @#AAFFAA: inclusion   | @#AAFFAA: $A:\mathrm{Ob}_{\bf D}$ |
| @#AAFFAA: inclusion   | @#AAFFAA: $\phi:{\bf C}[FB,Z]$ |
| @#FFFDDD: for all     | @#FFFDDD: $B:\mathrm{Ob}_{\bf D}$ |
| @#FFFDDD: for all     | @#FFFDDD: $\psi:{\bf C}[FA,Z]$ |
| @#DDDDDD: range       | @#DDDDDD: $f:{\bf D}[A,B]$ | 
| @#55EE55: postulate   | @#55EE55: $\exists_!f.\ \psi=\phi\circ F(f)$ |

==== Discussion ====
=== Terminology ===
Note that the name "terminal //morphisms//" for $\langle B,\phi\rangle$ is slightly confusing, because the data is not just the morphism $\phi$ going from $F(B)$ to $Z$, but also the object $B$. 

=== Idea ===
You want to specify a smaller world within ${\bf C}$. You do this by setting up another category ${\bf D}$ and mapping it into ${\bf C}$ with a functor $F$. The image of $F$ is your smaller world. 

For a fixed object $Z$, a universal morphism $\phi$ is then defined by demanding that every arrow from this small world which tries to connect $Z$, must pass through it. In other words (and now I just state the definition): For all objects $B$ in ${\bf D}$, if $\psi$ is an arrow in ${\bf C}$ from $FB$ to $Z$, then there must be an arrow $f$ within ${\bf D}$, so that $\phi$ is really just a combination of "small world business" $F(f)$, followed by the kind of gate function $\phi$, finally leading to $Z$. 

For the reason that everything going on in the image of $F$ must pass to $Z$ only through $\phi$, one says $\phi$ is the terminal morphism "from the functor $F$ to the object $Z$".

== Example: The exponential object and currying ==
So you have a function $\psi:X\times Y\to Z$ and you want to be able to do partial function application, i.e. make sense of just passing an argument of $X$ to $\psi$ and leave the second component unevaluated. In plain English, we need the function space which contains the half-evaluated function. To make use of it, we also need the evaluation function, which when passed the half-evaluated function and an argument of $Y$ returns the same as what $\psi$ would do.

It's done as follows: We have $Z:\mathrm{Ob}_{\bf C}$. Now fix any "second argument space" $Y$. Define the object map of the auto-functor $F$ as $FA:=A\times Y$ and its function map by $F(f):=f\times\mathrm{id}_Y$. Now we are done by asking for the terminal morphism from $F$ to $Z$: This exactly means the category must contain a function object, let's call it $Z^Y$, so that for any $\psi:X\times Y\to Z$ (which is $\psi:FX\to Z$) there is a function $f$, which chooses a function $F(f)(x)$ in $Z^Y$, so that $\psi$ can be written as first passing $\langle x,y\rangle:X\times Y$ to $\langle F(g)(x),y\rangle$ and then evaluates this via $\mathrm{eval}(F(f)(x),y):=\left(F(f)(x)\right)(y)$.

{{exponentialobject-01.png}}

(The left side is in ${\bf D}$, the right is in ${\bf C}$ and $f$ is called $\lambda g$ here.)

As a side note: As this works for all $Z$, this gives rise to a hom-class adjunction of the above functor $F$ and the one mapping $Y$ to $Z^Y$. The categorical currying is hence  
$\mathrm{hom}(X\times Y,Z)$ being isomorphic to $\mathrm{hom}(X,Z^Y)$. The nice thing is, of course, that this doesn't just work for categories with function, but the same construction also works when reasoning about logic, where currying then is the tautology 
$\left((A\land B)\implies C\right)\Leftrightarrow \left(A\implies(B\implies C)\right)$.

=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Universal_property|Universal property]], [[http://en.wikipedia.org/wiki/Exponential_object|Exponential object]]
==== Parents ====
=== Context ===
[[Functor]]
=== Requirements ===
[[Product type]]