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]$):

- 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.
- "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?