   There is a considerable literature on category theory in relation to proof theory, and, following seminal work by Lawvere, Lambek and others (see Lambek and Scott, 1986, and the references therein), category itself can be viewed as a kind of abstract proof theory. If one looks at an arrow A → B in a category as a kind of abstract proof of B from A, we have a representation which goes beyond pure derivability of B from A (as the arrow has its individuality), but does not deal with the particular syntactic structure of this proof. For intuitionistic systems, proof-theoretic semantics in categorial form comes probably closest to what denotational semantics is in the classical case.