Hi, I have a simple question concerning the adjoining of intedeterminates to cartesian (closed) categories. Before asking the question I describe the two results I am interested in then state my question. It is possible to adjoin an intedeterminate arrow X: 1 -> C to a cartesian (closed) category as follows: Proposition 1: If C is a cartesian (closed) category, X: 1 -> C an intedeterminate, and I: C -> C[X] is cartesian (closed) functor, there exists a unique cartesian functor G: C[X] -> D, such that G(X) = d and the following diagram commutes: I C -------> C[X] \ | \ | \ | \ | \ | F \ | G \ | \ | \ | \ | \ | D, where D is a cartesian category, F: C -> D is a cartesian functor, and d: 1 -> F(C). The proof of this proposition can be given directly or via an alternative definition in terms of the reader comonad and the corresponding Klesli construction (personally I find the later simply and more intuitive). As far as I am aware these constructions were originally given by Lambek [lam74], proofing the corresponding deduction theorem for cartesian closed categories, and revised by Lambek and Scott [lam&sco86]. Although the above result is well known it seems that the result of adjoining an intedeterminate object to a cartesian closed category, in particular it's proof, is not so well known. This result may be stated as follows: Proposition 2: If C is a cartesian (closed) category, X an interterminate, and I: C -> C[X] is a functor, there exists a unique cartesian (closed) functor G: C[X] -> D, such that G(X) = D, and the following diagram commutes: I C -------> C[X] \ | \ | \ | \ | \ | F \ | G \ | \ | \ | \ | \ | D, where D is a cartesian (closed) category, F: C -> D is a cartesian closed functor, and D is in Obj(D). The problem is that it is not clear how to proof Proposition 2. I believe that it is possible to use results from the work of Kelly and various colleagues in the field of Two-dimensional universal algebra [back89]. However, I was hoping that there may be a more direct route to proving this result, which does not rely on the Two-dimensional monad theory. My question is simply this: Is there a more direct, and hopefully simpler, proof of Proposition 2? Thank you for any help you can provide on this subject. Best wishes Ben -------- Benedict R. Gaster. Languages and Programming Group, University of Nottingham. A thing of beauty is a joy forever. -- John Keats (1795--1821). --------------------------------------------------------------------------- References: [back89] R. Backwell and G.M. Kelly and A.J. Power Two-Dimensional Monad Theory Journal of Pure and Applied Algebra year = 1989 [lambek74] J. Lambek Functional Completeness of Cartesian Categories Annals of Mathematical Logic} 1974 [lam&sco86] J. Lambek and P. J. Scott Introduction to higher order categorical logic Cambridge University Press Cambridge studies in advanced mathematics 7 1986