Adjoining an arrow to a CCC

Question

I just started reading Lambek and Scott's book "Introduction to higher-order categorical logic".

Right now I am reading Part I, section 5 (Polynomial categories). They explain two ways of adjoining an inderterminate arrow $x : A_0 \to A$ to a category $\mathcal{A}$ (called $\mathcal{A}[x]$):

1. Take the underlying graph of $\mathcal{A}$ adjoin $x : A_0 \to A$ to it, and then form the cartesian closed category freely generated by the new graph.
2. "Equivalently"; form a deductive system (some kind of graph) with objects as the objects of $\mathcal{A}$ and arrows freely generated from the arrows of $\mathcal{A}$ and the new arrow $x : A_0 \to A$, using the application, "initial arrow", pairing, projections, eval and currying, and then they impose the appropiate equations of a CCC and those of $\mathcal{A}$.

I don't see these constructions are infact equivalent. For example, suppose I have two objects $A$ and $B$ in $\mathcal{A}$. Using the construction 1, you end up with two forms of $A^B$ in $\mathcal{A}[x]$: the original one (already avaiable in $\mathcal{A}$) and the one generated freely. Using construction 2, I think you end up with only one form of $A^B$: the original one.

Why do they mean by equivalently? That those categories are equivalent? What's the standard way of constructing this category theory?

Answer 1

They mean this: given a cartesian closed $\mathcal{A}$ and objects $A, B$ of $\mathcal{A}$, the inclusion $i: \mathcal{A} \to \mathcal{A}[x]$ is universal with respect to strict cartesian closed functors $F: \mathcal{A} \to \mathcal{C}$ to cartesian closed categories $\mathcal{C}$ that come equipped with a specified arrow $\phi: F(A) \to F(B)$. (I don't have their book to hand, but I think they always deal with chosen products, chosen exponentials, and strict preservation of structure, as they find that more convenient for their purposes. However, such strictness can be relaxed so as to be 2-categorically more appropriate.) In other words, $\mathcal{A}[x]$ comes equipped with a specified "indeterminate" arrow $x: i(A) \to i(B)$, and $F$ can be extended uniquely to a strict cartesian closed functor $\hat{F}: \mathcal{A}[x] \to \mathcal{C}$ that takes $x$ to $\phi$.

Since they are working strictly, considering ccc's as objects of a 1-category, equivalence here actually means isomorphism (a strict ccc functor that is invertible).

In any case, the inclusion $i: \mathcal{A} \to \mathcal{A}[x]$ is required to be a strict cartesian closed functor. So it preserves exponentials (strictly, in their setting): $i(A^B) = i(A)^{i(B)}$. In other words, the "two" exponentials coincide.

Their "functional completeness theorem" gives a very elegant construction of the polynomial ccc $\mathcal{A}[x]$ as a Kleisli category construction. You can find some details on this in the nLab, although the strictness assumptions are not used there.

Answer 2

This question is really old, but in case anyone stumbles onto it, I wanted to provide a possibly more understandable and clear categorical representation of $\cal{A}[x]$ given by adding $x \colon A_0 \to A_1$ that helped me get a clearer picture of what is happening and hence to answer the last query in the post.

Note that the theory of CCC's is an essentially algebraic theory. Now, given that theory, postulate constants $A_1, A_0$ and $x \colon A_0 \to A_1$ in the appropriate sorts. Name the theory $CCC[x]$.

We have a free-forgetful adjunction between our two categories of models of essentially algebraic theories. The category $CCC[x]$ consists of cartesian closed categories with a selected morphism $x$ in one its homsets. Morphisms are functors preserving said structure on the nose, i.e. these are cartesian closed functors that preserve the selected morphism.

Note that the unit $\eta \colon 1 \Rightarrow UF$ will pointwise have the same universal property as the one that the inclusion $A \to A[x]$ has as described by Proposition 5.1 in the book.

In particular, $F(A) \cong A[x]$

To check its relation to the free graph construction described in the the beginning of Section 5, one may look at all the free $\dashv$ forgetful adjunctions arizing from the corresponding essentially algebraic theories.