Embedding of a Free Cartesian Closed Category into the Category

of Sets

Djordje <=Cubri?c

Abstract

We show that every free cartesian closed category can be faithfully mapped to the category of sets. For that we use a Church-Rosser property of the appropriate typed lambda calculus.

1 Introduction

The goal of this paper is to prove the following theorem:

Theorem 1.1 Let C be a free cartesian closed category. Then there exists a faithful structure preserving functor F : C ! Set.

Informally, a free cartesian closed category is a cartesian closed category freely generated by objects and arrows between generated objects.

Some consequences of the above result are that various extensions of cartesian closed structure do not impose additional equalities among arrows: let I : C ! B(C) be the canonical map from a free cartesian closed category C to the free Boolean topos B(C) generated by C then I is faithful. But perhaps more important is that it confirms our intuition that cartesian closed categories indeed axiomatize the cartesian closed structure of sets. (In everyday practice" it means that a diagram commutes in every cartesian closed category if and only if it commutes in Set.)

Concerning the history of Theorem 1.1, we note that the problem whether it was true had been raised, along with analogous problem involving monoidal closed categories, by M. Barr and others, many years ago. [16] gives a proof that for every two arrows in a free cartesian closed category without free arrows there is a structure preserving functor into the category of finite sets which distinguishes these two arrows; in the proof the (then unrepaired) Mints' reductions are used.

Theorem 1.1 is formally analogous to results in [15] and [6], each of which gives representations, in the form of structure-preserving functors, of cartesian-closed and richer structures in certain toposes; in place of faithfulness, other conditions are imposed on the representation. The methods in this paper are quite different from these of [15] or [6].

The above theorem is proved using connection between cartesian closed categories and typed >=-calculi for the early history" of the subject see the comments in [10]. A key technical step is that in a free cartesian closed category one can faithfully adjoin infinitely many maps 1 ! C for every object C. This is shown with the help of a system of reductions suggested by G. Mints. Unfortunately the original paper contains some mistakes, as V. Harnik pointed out to us, see the remark 4.17; since we think that these reductions are very interesting on their own right, we repair Mints' proof (of confluence as well as normalization). Also, an important ingredient in the proof is a variant of H. Friedman's completeness result for (a variant of) typed >=-calculus.

We obtained the main theorem in spring 1990 and I gave a talk on that on a McGill seminar organized by Prof. Lambek. However, I was using Mints result without noticing this mistake in