Coherence in cartesian closed categories and the generality of proofs

We introduce the notion of an alphabetic trace of a cut-free intuitionistic prepositional proof and show that it serves to characterize the equality of arrows in cartesian closed categories. We also show that alphabetic traces improve on the notion of the generality of proofs proposed in the literature. The main theorem of the paper yields a new and considerably simpler solution of the coherence problem for cartesian closed categories than those in 11, 14].This research was supported in part by N.S.E.R.C. Grant A-8224 and F.C.A.R. Grant EQ-3491. The author is attached to the Centre interuniversitaire en études catégoriques, McGill University, Montreal.