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$?

  • $\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 White Jul 11 '13 at 0:41

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.