# Adjoining an arrow to a CCC

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?

-
I think they mean the two categories are equivalent, not that they are equal. – François G. Dorais Jul 14 '13 at 21:06

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.

-
How does the construction 1 can have such functor $i$? When they define the construction of a free cartesian closed category over a graph, they add new objects for products, exponentials, and terminal. How can you have $i(A^B) = i(A)^{i(B)}$? – tsctsc Jul 14 '13 at 22:26
Okay, I now see what you're referring to. Courtesy of Google books, I'm looking now at page 57, the first paragraph of section 5. It seems they really botched the first description badly. My advice would be to ignore that bit you copied into 1., and read on. You can see from subsequent text that they really mean for the inclusion of $A$ into $A[x]$ to preserve ccc structure strictly. You will see the "linguistic" construction of $A[x]$, and the conceptual Kleisli construction which is the basis for their functional completeness, and which I think you will find pretty. – Todd Trimble Jul 14 '13 at 22:54
I'm starting to read that part. Thanks! – tsctsc Jul 15 '13 at 1:21