Barry Jay's question

Barry Jay's question

[Michael Barr]

Unless I am missing something, it seems to me that for any CCC C with
finite limits and any finite category I, the functor category C^I is a
CCC.  You can also replace finite by any cardinal if you do it in both
places.  The argument is roughly this.  Let |I| denote the discrete
category with the objects of I.  The inclusion |I| --> I induces U: C^I
--> C^{|I|} and the limits imply the existence of a right adjoint R of U.
Since U also preserves limits, the cotriple (UR,e,d) preserves finite
limits.  It is easy to see that U is cotripleable and that C^{|I|} is a
CCC and, hence, so is C^I.  For define A -o RC = R(UA -o C).  For a
general object B, the line B --> URB ==> URURB is an equalizer and you can
define A -o B as the equalizer of A -o URB ==> A -o URURB.  

Michael


-------------------------------------------------------------------
History shows that the human mind, fed by constant accessions of
knowledge, periodically grows too large for its theoretical coverings, and
bursts them asunder to appear in new habiliments, as the feeding and
growing grub, at intervals, casts its too narrow skin and assumes
another... Truly the imago state of Man seems to be terribly distant, but
every moult is a step gained. 

- Charles Darwin, from "The Origin of Species"