Locally Cartesian Closed implies Cartesian Closed

176 Views Asked by At

We follow Awodey's definition (page 235, Category Theory, 2nd ed.) of locally cartesian closed categories:

A category $\mathcal E$ is locally cartesian closed provided $\mathcal E$ has a terminal object, 1, and for each $\mathcal E$-arrow $f\colon A\to B$, the post-composition functor $\Sigma_f\colon \mathcal E_{/A}\to \mathcal E_{/B}$ has a right adjoint $f^*$ which also admits a right adjoint $\Pi_f$, i.e., we have the following adjoint situation: $$ \Sigma_f\dashv f^*\dashv \Pi_f\colon \mathcal E_{/A}\to \mathcal E_{/B}. $$

I want to show that if $\mathcal E$ is locally cartesian closed, it is also cartesian closed. Following Awodey, we want to show for each $B\in \mathcal E$, the terminal morphism $B\colon B\to 1$ gives us product and exponential constructions by $$ A\times B=\Sigma_BB^*(A) \quad \text{ and } \quad B^A=\Pi_B B^*(A). $$ From the adjoint, we know that proving either of the above equalities will give us the other since $$\mathcal E(\Sigma_BB^*A,X)\cong \mathcal E_{/B}(B^*A,B^*X)\cong \mathcal E(A,\Pi_BB^*X)$$naturally for each $A,B,X\in \mathcal E$. I am not sure how to proceed. Should I attempt to show the universality of $\Sigma_B B^*A$? If so, I can't seem to find the proper projections. One would be the counit: $\varepsilon_A\colon \Sigma_BB^*A\to A$ I assume. What would be the other projection $\Sigma_BB^*A\to B$?