Cut elimination in categories (Q1817695)

The book is an introduction to categorical proof theory. After the presentation of basic notions (category, functor, natural transformation) from the proof-theoretical point of view, main attention is paid to the notion of adjunction together with the related notion of comonad (one may as well consider monads). It is shown that all these notions can be formulated in such a way that the (standard) equalities between arrows are necessary and sufficient conditions for the composition (i.e., cut) elimination in freely generated structures corresponding to these notions. This means, in particular, that every arrow in categories involved in freely generated adjunctions and comonads can be represented by a term that does not contain composition. Moreover, such a term has normal form unique for the arrow. The composition-free normal form serves also to demonstrate that strengthening the notions of adjunction and comonad with any new equality between arrows would trivialize these notions. The difference between these composition-free formulations of categorical notions and standard formulation is that natural transformations are not conceived as families of arrows, but as operations on arrows. The book has an introduction and six chapters. In chapter 1 cut elimination in free categories generated by arbitrary graphs is considered. (In the form of ``cut disintegration'', which is local in contrast to Gentzen's global approach.) In chapter 2 it is shown how the notion of functor (and semifunctor) can be characterized by ``cut disintegration''. In chapter 3 the same approach is developed for natural transformations. Chapter 4 is central for the book. In this chapter free adjunctions are considered. In chapter 5 the author considers free comonads (from a logical point of view they precede in a way the monads). These chapters contain a survey and comparison of existing definitions of adjunction and comonad. Their behaviour w.r.t. cut elimination is studied. As an application of cut elimination results it is shown that the notion of adjunction is maximal in the sense that strengthening this notion with any new equality between arrows would trivialize it. The same is shown for comonads in chapter 5. In chapter 6 the application of the above to a special case of adjunction is considered (the adjunction involving the product in cartesian categories). Concerning the ``state of the art'' in categorical proof-theory, the book does not try to be exhaustive. The presentation is quite accessible and treats in original way several fundamental aspects (adjointness, comonads...). Clear and detailed proofs are provided.