When you start with a CCC $C$, take the underlying graph of $C$ via the forgetful $U : Cat \to Graph$, and then construct the free CCC over $U(C)$ via $Free : Graph \to Cat$: what's the relationship between the original cartesian product object of two objects $A$ and $B$ in $C$ through inclusion in $Free(U(C))$, and the "constructed" product in $Free(U(C))$ between the same objects $A$ and $B$?
1
-
$\begingroup$ Are you aware of Kelly's \emph{A Unified Treatment of Transfinite Constructions for Free Algebras, Free Monads, Colimits, Associated Sheaves, and so on}? The answer is almost certainly in there. See this link: journals.cambridge.org/… $\endgroup$– David WhiteJul 11, 2013 at 0:41
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
I would say: none in general. Let's denote product, pairs, and projections in $\mathcal{C}$ by juxtaposition, parentheses, $p$, and $q$, respectively, while we denote product and projections in $\mathit{Free}(\mathcal{C})$ by $\times$, angle brackets, $\pi$, and $\pi'$, respectively. Consider any object $t \in \mathcal{C}$. You can construct a morphism $t t \to t \times t$ using the simply-typed $\lambda$-term
$$x : t t \vdash \langle p, q \rangle : t \times t.$$
However, the $\eta$ law for products does not apply, as $p$ and $q$ are not the projections corresponding to $\langle - \rangle$.
Perhaps more formally, juxtaposition is generally not a product in $\mathit{Free}(\mathcal{C})$. To see this, try to form a pairing of $\mathit{id} : t \to t$ with itself, where $\mathit{id}$ is an identity in $\mathcal{C}$. This would be $(\mathit{id},\mathit{id}) : t \to t t$. However, when you compose it with, say, $p$, this is composition in $\mathit{Free}(\mathcal{C})$, not $\mathcal{C}$, so that the result is different from $\mathit{id}$. Another symptom is that there no pairing for the identity of $t$ in $\mathit{Free}(\mathcal{C})$ with itself.
This is not very formal, but I think could be turned into a proof.
