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?



Adjoining an arrow to a CCC
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](http://ncatlab.org/nlab/show/cartesian+closed+category#functional_completeness_theorem_31) on this in the nLab, although the strictness assumptions are not used there. 


