Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
    
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/… –  David White Jul 11 '13 at 0:41

1 Answer 1

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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