#
Categories for computation in context and unified logic

by R.F. Blute, J.R.B. Cockett, and R.A.G. Seely

(Presented to Peter Freyd to mark the occasion of his 60th birthday)

### Abstract

In 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.