6
$\begingroup$

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?

$\endgroup$
2
  • 1
    $\begingroup$ I think they mean the two categories are equivalent, not that they are equal. $\endgroup$ Jul 14, 2013 at 21:06
  • 1
    $\begingroup$ The same thing confused me too. It is even worse, the free CCC of $(UA)[x]$ will not even have a well defined functor $A\to F(UA[x])$, because forming the free cartesian category from a graph doesn't make the identifications $f\circ g =h$ which hold in the category $A$ has. Also it doubles the exponentials and products etc.. I believe it is best to invent a new deductive system to describe $A[x]$. $\endgroup$
    – Nico
    Jun 9, 2022 at 16:26

2 Answers 2

7
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ 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)}$? $\endgroup$
    – tsctsc
    Jul 14, 2013 at 22:26
  • 4
    $\begingroup$ 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. $\endgroup$
    – Todd Trimble
    Jul 14, 2013 at 22:54
  • $\begingroup$ I'm starting to read that part. Thanks! $\endgroup$
    – tsctsc
    Jul 15, 2013 at 1:21
0
$\begingroup$

This question is really old, but in case anyone stumbles onto it, I wanted to provide a possibly more understandable and clear categorical representation of $\cal{A}[x]$ given by adding $x \colon A_0 \to A_1$ that helped me get a clearer picture of what is happening and hence to answer the last query in the post.

Note that the theory of CCC's is an essentially algebraic theory. Now, given that theory, postulate constants $A_1, A_0$ and $x \colon A_0 \to A_1$ in the appropriate sorts. Name the theory $CCC[x]$.

We have a free-forgetful adjunction between our two categories of models of essentially algebraic theories. The category $CCC[x]$ consists of cartesian closed categories with a selected morphism $x$ in one its homsets. Morphisms are functors preserving said structure on the nose, i.e. these are cartesian closed functors that preserve the selected morphism.

Note that the unit $\eta \colon 1 \Rightarrow UF$ will pointwise have the same universal property as the one that the inclusion $A \to A[x]$ has as described by Proposition 5.1 in the book.

In particular, $F(A) \cong A[x]$

To check its relation to the free graph construction described in the the beginning of Section 5, one may look at all the free $\dashv$ forgetful adjunctions arizing from the corresponding essentially algebraic theories.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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