Categorical interpretation of logical derivations and some its applications to algebra

We consider certain applications of proof theory to the study of algebraic categories. The case usually studied in literature is the case of free categories with additional structure. In this paper we consider several problems in non-free categories, such as the problem of full coherence, the problem of dependency of diagrams, the problem of description of arbitrary natural transformations, that show that the applications of proof theory to categories may go much farther. Bibl. – 18 titles.