Closed categories and the theory of proofs

The main aim of this article is to suggest a translation of the simplest concepts of category theory into the language of (structural) theory of proofs, to use this translation to simplify the proofs of some known results [1], and to obtain two new ones: the coherence theorem for canonical morphisms in (nonmonoidal, nonsymmetric) closed categories [2], and the solution of the problem of equality of canonical morphisms. Extensions of these results to monoidal closed, symmetric closed, and monoidal symmetric closed categories are sketched. The decision procedure is obtained by means of a correct and faithful translation of canonical morphisms into an expansion of the $\lambda$-language, which has the tools for a special account of “superfluous” premises of implications (the thinning rule). The expansions of the $\lambda$-language which have so far appeared in the literature have not possessed this facility.