Categories for computation in context and unified logic

AbstractIn this paper we introduce context categories to provide a framework for computations in context. The structure also provides a basis for developing the categorical proof theory of Girard's unified logic. A key feature of this logic is the separation of sequents into classical and linear zones. These zones may be modelled categorically as a context/computation separation given by a fibration. The perspective leads to an analysis of the exponential structure of linear logic using strength (or context) as the primitive notion.Context is represented by the classical zone on the left of the turnstile in unified logic. To model the classical zone to the right of the turnstile, it is necessary to introduce a notion of cocontext. This results in a fibrational fork over context and cocontext and leads to the notion of a bicontext category. When we add the structure of a weakly distributive category in a suitably fork fibred manner, we obtain a model for a core fragment of unified logic.We describe the sequent calculus for the fragment of unified logic modelled by context categories; cut elimination holds for this fragment. Categorical cut elimination also is valid, but a proof of this fact is deferred to a sequel