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"