📝Category Theory: Function object

Universal construction

$a \Rightarrow b \text{ is a function object} \iff \forall z, \exists! h: z \to (a \Rightarrow b) \ni g = eval \circ (h \times id)$

• This relies on that a morphism between two products ($h \times id: (z \times a) \to ((a \Rightarrow b) \times a)$) can be constructed as a product of two morphisms ($h$ and $id$), so that we know that it is a correct way to obtain $(a \Rightarrow b) \times a$ from $z \times a$ using $h: z \to (a \Rightarrow b)$