In Categories, Types and Structures, authors talk about exponential objects in section 2.3.1.

Let $C$ be a Cartesian category, and $a,b \in Ob_C$. The exponent of $a$ and $b$ is an object $b^a$ together with a morphism $eval_{alb}: b^a \times a\rightarrow b$ (evaluation map), and for every object $c$ an operation $\Lambda_c : C[c\times a,b]\rightarrow C[c, b^a]$ such that for all morphisms $f: c\times a\rightarrow b$, $h:c\rightarrow b^a$, the following equation holds:
$\beta. eval_{a,b} \circ (\Lambda (f)\times id_a )=f$
$\eta. \Lambda_c(eval_{a,b}\circ(h\times id_a))=h$

Can you please show me the steps to derive the last two equations?

  • 2
    $\begingroup$ This is a (possible) definition of an exponential object; what do you want to prove exactly? $\endgroup$
    – cody
    Jul 22, 2022 at 20:15

1 Answer 1


The following morphism and commuting morphisms explain why those two equations hold:

$h:c\rightarrow b^a$

commuting morphisms:

$eval: b_a\times a\rightarrow b$
$f:c\times a\rightarrow b$
$h\times id: c\times a\rightarrow b^a\times a$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.