|
Abstract:
|
In this dissertation methods of the proof theory are used to investigate coherence in some
categories. Moreover, it is shown what the categorical notion of coherence means in the categorial
proof theory. The thesis consists of three chapters. MacLane’s results for monoidal
categories and symmetric monoidal categories are extended in Chapter 1 of the dissertation to
some other categories with multiplication: relevant categories, affine categories and symmetric
monoidal categories. All the results are formulated in terms of natural transformations
equipped with “grafs” (g-natural transformations). It is proved, as consequences of these results,
that relevant categories, affine categories and symmetric monoidal categories have the
coherence property. Moreover, using these results, some basic relations between the free
categories of these classes of categories are presented in Chapter 2 of the dissertation. In
Chapter 3, an extension of the notion of dinatural transfomation is introduced in order to give
a criterion of preservation of dinaturality under composition. An example of an application is
given by proving that all cartesian closed canonical categories transformations are dinatural.
Finally, an alternative sequent system for a fragment of intuitionistic propositional logic is
introduced as a device, and a cut-elimination procedure is established for this system. |