Cut elimination in adjuncion

Abstract

The notion of adjunction is formulated so that for every arrow in freely gener-ated adjunctions there is a composition-free term for this arrow, which can be brought into a normal form unique for the arrow. In this formulation, natural transformations are not conceived as families of arrows, but as operations on arrows. Composition elimination is the form Gentzen's cut elimination takes in categories. The composition-free normal form serves to obtain simple geometri-cal decision procedures for the commuting of diagrams. It serves also to show that adding to the notion of adjunction any new equality between arrows in the language of free adjunctions would trivialize this notion.