Coherence for cartesian closed categories: A sequential approach

Abstract

A coherence theorem states that the arrows between two particular objects in free categories are unique. In this paper, we give a direct proof for cartesian closed categories (CCC's) without passing to typed lambda calculus. We first derive categorical combinators for CCC's together with their equations directly from the adjoint functors defining CCC's. Then categorical interpretation of the intuitionistic sequent calculus is regarded as the construction of free CCC's. Each arrow is generated along the proof derivation in form of categorical combinators. The system enjoys the cut-elimination theorem and we can use various proof-theoretic techniques such as Kleene's permutability theorem. The coherence is proved by showing that the reconstruction of derivations for the given class of arrows is deterministic and unique up to equivalence.