Adjoining intedeterminates to cartesian categories

[categories <cat-dist@mta.ca>]

Date: Tue, 25 Nov 1997 10:51:06 +0000
From: Benedict R. Gaster <brg@Cs.Nott.AC.UK>


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